proposition: Lemma Qhomographic_denom_nonzero_correct_1 : forall (c d : Z) (q : Q), Qplus (Qmult c q) d <> Zero -> Qhomographic_denom_nonzero c d q.
proof: Proof. abstract (intros c d [| p| p] H_denom; [ apply Qhomographicok0; trivial; intros H; apply H_denom; rewrite H; replace (Z_to_Q 0) with Zero; trivial; abstract ring | apply Qhomographicok1 with p; trivial; apply Qhomographic_sg_denom_nonzero_correct_2; assumption | apply Qhomographicok2 with p; trivial; apply Qhomographic_sg_denom_nonzero_correct_2; intro H; apply H_denom; replace (Qmult c (Qneg p)) with (Qmult (- c)%Z (Qpos p)); trivial; rewrite Z_to_Qopp; rewrite Qopp_Qpos; abstract ring ]). Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)