proposition: Theorem divA_A0_l : forall (a : A) (nZa : ~ eqA a A0), eqA (divA A0 a nZa) A0.
proof: Proof. intros a nZa; apply eqA_trans with (y := divA (multA A0 a) a nZa). apply divA_eqA_comp with (1 := cs); auto. apply eqA_trans with (y := multA A0 (divA a a nZa)); auto. Qed.