proposition: Theorem invA0_inv : forall a : A, eqA a (invA (invA a)).
proof: Proof. intros a. apply eqA_trans with (y := plusA a A0); auto. apply eqA_trans with (y := plusA A0 a); auto. apply eqA_trans with (y := plusA (plusA (invA a) (invA (invA a))) a); auto. apply eqA_trans with (y := plusA (plusA (invA (invA a)) (invA a)) a); auto. apply eqA_trans with (y := plusA (invA (invA a)) (plusA (invA a) a)); auto. apply eqA_trans with (y := plusA (invA (invA a)) (plusA a (invA a))); auto. apply eqA_trans with (y := plusA (invA (invA a)) A0); auto. Qed.