proposition: Lemma Inverses_congl : Map2_congl_law Inverses_comp.
proof: Proof. unfold Map2_congl_law in |- *. intros x y z. elim x; elim y; elim z; simpl in |- *. intros a a' p p' a0 a0' p0 p0' a1 a1' p1 p1' H. unfold Inv_comp_elt_l, Inv_comp_elt_r in |- *; simpl in |- *. apply (Prf_map2_congl (Mop A) (b1:=a1) (b2:=a0) a); trivial. Qed.
imports: Group