proposition: Lemma equal_by_zero_sum x y : x - y = 0 <-> x = y.
proof: Proof. split; intros E. - rewrite <- (plus_0_l y). rewrite <- E. rewrite <-simple_associativity. rewrite left_inverse. apply symmetry,right_identity. - rewrite E. apply right_inverse. Qed.
imports: HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra