proposition: Theorem divA_nZ : forall a b : A, ~ eqA b A0 -> forall nZa : ~ eqA a A0, ~ eqA (divA b a nZa) A0.
proof: Proof. intros a b H' nZa; red in |- *; intros H'1; auto. case H'; apply eqA_trans with (y := multA (divA b a nZa) a); auto. apply divA_is_multA with (1 := cs); auto. apply eqA_trans with (y := multA A0 a); auto. Qed.