proposition: Theorem divA_multA_comp_l : forall (a b c : A) (nZc : ~ eqA c A0), eqA (divA (multA a b) c nZc) (multA a (divA b c nZc)).
proof: Proof. intros a b c nZc; apply eqA_trans with (y := divA (multA b a) c nZc); auto. apply eqA_trans with (y := multA (divA b c nZc) a); auto. apply divA_multA_comp_r with (1 := cs); auto. Qed.