proposition: Lemma cs_unique_unit : forall (S:CSemiGroup) (e f:S), (is_unit S e) /\ (is_unit S f) -> e[=]f.
proof: Proof. intros S e f. unfold is_unit. intros H. elim H. clear H. intros H0 H1. elim (H0 f). clear H0. intros H2 H3. elim (H1 e). clear H1. intros H4 H5. astepr (e[+]f). astepl (e[+]f). apply eq_reflexive. Qed.
imports: CoRN.algebra.CSetoidInc