proposition: Lemma Midl_Inverses : Monoid_idl Inverses_op Inverses_unit.
proof: Proof. red in |- *. simple induction x; simpl in |- *; intros. unfold Inverses_eq, Inv_comp_elt_l in |- *; simpl in |- *. apply (Prf_monoid_idl Inv_elt_l0). Qed.
imports: Group