proposition: Lemma MONOID_unit_unique : forall e : E, (forall x : E, Equal (sgroup_law _ x e) x) -> (forall x : E, Equal (sgroup_law _ e x) x) -> Equal e (monoid_unit E).
proof: Proof. intros e H' H'0; try assumption. apply Trans with (sgroup_law _ e (monoid_unit E)); auto with algebra. apply Sym. apply MONOID_unit_r. Qed.
imports: Monoid_cat