proposition: Lemma Mass_Inverses : Monoid_ass Inverses_op.
proof: Proof. red in |- *. simple induction x; simple induction y; simple induction z; simpl in |- *; intros. unfold Inverses_comp, Inv_comp_elt_l, Inv_comp_elt_r in |- *; simpl in |- *. apply (Prf_monoid_ass Inv_elt_l0 Inv_elt_l1 Inv_elt_l2). Qed.
imports: Group