proposition: Theorem multA_invA_com_r : forall a b : A, eqA (multA a (invA b)) (invA (multA a b)).
proof: Proof. intros a b; apply eqA_trans with (y := multA (invA b) a); auto. apply eqA_trans with (y := invA (multA b a)); auto. Qed.