proposition: Lemma Qmult_resp_nonzero : forall x y : Q, x <> Zero -> y <> Zero -> Qmult x y <> Zero.
proof: Proof. intros x y Hx Hy Hxy; generalize (Q_integral _ _ Hxy); intros [H| H]; [ apply Hx | apply Hy ]; assumption. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)