proposition: Lemma Inverses_congr : Map2_congr_law Inverses_comp.
proof: Proof. unfold Map2_congr_law in |- *; simple induction a1; simple induction a2; simpl in |- *. intros b0 b0' p0 p0' z; elim z. intros b1 b1' p1 p1' H. unfold Inv_comp_elt_l, Inv_comp_elt_r in |- *; simpl in |- *. apply (Prf_map2_congr (Mop A) (a1:=Inv_elt_l0) (a2:=b0) b1); trivial. Qed.
imports: Group