proposition: Theorem A_sep : forall a b : A, eqA (multA a b) A0 -> eqA a A0 \/ eqA b A0.
proof: Proof. intros a b H'; case (eqA_dec a A0); auto; case (eqA_dec b A0); auto. intros nZb nZa; case nZa. apply eqA_trans with (y := multA (divA a b nZb) b); auto. apply divA_is_multA with (1 := cs); auto. apply eqA_trans with (y := divA (multA a b) b nZb); auto. apply eqA_sym; apply divA_multA_comp_r with (1 := cs); auto. apply eqA_trans with (y := divA A0 b nZb); auto. Qed.