Consisent direction for `CMRA_NAME_op` lemmas.
I've noticed something which can be seen as a discrepancy in the lemmas.
These ones follow the pattern "constructor of the multiplication is equal to the multiplication of constructors".
Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b. Definition Some_op a b : Some (a ⋅ b) = Some a ⋅ Some b := eq_refl.
These ones go the other way around: "multiplication of constructors is equal to the constructor of multiplications":
Lemma Cinl_op a a' : Cinl a ⋅ Cinl a' = Cinl (a ⋅ a'). Lemma Cinr_op b b' : Cinr b ⋅ Cinr b' = Cinr (b ⋅ b'). Lemma pair_op (a a' : A) (b b' : B) : (a, b) ⋅ (a', b') = (a ⋅ a', b ⋅ b').
Should this be changed or am I nitpicking and the (breaking) change will be too invasive?