proposition: Lemma cg_minus_wd : forall x x' y y' : G, x [=] x' -> y [=] y' -> x [-] y [=] x' [-] y'.
proof: Proof. intros x x' y y' H H0. unfold cg_minus in |- *. Step_final (x[+] [--] y'). Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids