`grind` annotations for OFE operations

[markusdemedeiros]

In our development we have quite a few calc blocks such as:

theorem Agree.includedN {x y : Agree α} : x ≼{n} y ↔ y ≡{n}≡ y • x := by
  refine ⟨fun ⟨z, h⟩ => ?_, fun h => ⟨y, h.trans op_commN⟩⟩
  have hid := idemp (x := x) |>.symm
  calc
    y ≡{n}≡ x • z := h
    _ ≡{n}≡ (x • x) • z := .op_l (hid n)
    _ ≡{n}≡ x • (x • z) := CMRA.op_assocN.symm
    _ ≡{n}≡ x • y := h.symm.op_r
    _ ≡{n}≡ y • x := op_commN

In my opinion, this is a great way to structure these proofs! I even like it better than the the Rocq version which uses setoid rewriting, because you're able to actually read these proofs, without trying to mentally reconstruct what effect each step has on the goal.

I think they could be made even better if the proof terms were (mainly) inferred, and I think that grind might be the right tool to do that. Is it possible to add grind annotations to our codebase so that the bulk of the steps in these calc blocks are all resolved by grind?