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