proposition: Lemma Opposite_map_law : Map_law Opposite.
proof: Proof. red in |- *; intros x y. elim x; elim y; simpl in |- *; unfold Inverses_eq in |- *; simpl in |- *. intros a a' aa' a'a b b' bb' b'b ba. apply Trans with (b' +_M Munit A). apply Midr. apply Trans with (b' +_M (a +_M a')). unfold ApMop in |- *; apply Map2_l. apply Sym; trivial. apply Trans with (y := b' +_M a +_M a'). apply Mass. apply Trans with (Munit A +_M a'). 2: apply Midl. unfold ApMop in |- *; apply Map2_r. apply Trans with (b' +_M b). 2: assumption. unfold ApMop in |- *; apply Map2_l. apply Sym; trivial. Qed.
imports: Group