proposition: Lemma Eq_abb'a' : forall a b a' b' : A, Inverses_rel a a' -> Inverses_rel b b' -> Inverses_rel (a +_M b) (b' +_M a').
proof: Proof. intros a b a' b' i j. red in |- *. apply Trans with (a +_M (b +_M (b' +_M a'))). apply Mass1. apply Trans with (a +_M a'). apply (Map2_l (Mop A) (b1:=b +_M (b' +_M a')) (b2:=a') a). apply Trans with (b +_M b' +_M a'). apply Mass. apply Trans with (Munit A +_M a'). apply (Map2_r (Mop A) (a1:=b +_M b') (a2:=Munit A) a'). apply j. apply Midl. apply i. Qed.
imports: Group