proposition: Theorem invA0_comp : forall a : A, eqA a A0 -> eqA a (invA a).
proof: Proof. intros a H'; apply eqA_sym; apply eqA_trans with (y := A0); auto. apply eqA_trans with (y := invA A0); auto. apply eqA_sym; apply invA0; auto. Qed.