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