x y : x - y = 0 <-> x = y. Proof. split; intros E. - rewrite <- (left_identity y). change (sg_op ?x ?y) with (0 + y). rewrite <- E. rewrite <-simple_associativity. rewrite left_inverse. apply symmetry,right_identity. - rewrite E. apply right_inverse. Qed.
Require Import Require Import