proposition: Lemma cg_minus_strext : forall x x' y y' : G, x [-] y [#] x' [-] y' -> x [#] x' or y [#] y'.
proof: Proof. intros x x' y y' H. cut (x [#] x' or [--] y [#] [--] y'). intro H0. elim H0. left; trivial. intro H1. right; exact (cs_un_op_strext G cg_inv y y' H1). apply bin_op_strext_unfolded with (csg_op (c:=G)). trivial. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids