proposition: Lemma Qhomographic_denom_nonzero_correct_2 : forall (c d : Z) (q : Q), Qhomographic_denom_nonzero c d q -> Qplus (Qmult c q) d <> Zero.
proof: Proof. abstract (intros c d q H_Qhomographic_denom_nonzero; induction H_Qhomographic_denom_nonzero; [ rewrite H; replace (Qmult c Zero) with Zero; [ idtac | abstract ring ]; rewrite Qplus_zero_left; replace Zero with (Z_to_Q 0); trivial; apply Z_to_Q_not_eq; assumption | rewrite H; apply Qhomographic_sg_denom_nonzero_correct_1; assumption | rewrite H; replace (Qmult c (Qneg p)) with (Qmult (- c)%Z (Qpos p)); [ apply Qhomographic_sg_denom_nonzero_correct_1; assumption | rewrite Z_to_Qopp; rewrite Qopp_Qpos; abstract ring ] ]). Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)