proposition: Lemma Qhomographic_sg_denom_nonzero_correct_1 : forall (c d : Z) (p : Qpositive), Qhomographic_sg_denom_nonzero c d p -> Qplus (Qmult c (Qpos p)) d <> Zero.
proof: Proof. intros c d p H_Qhomographic_sg_denom_nonzero. induction H_Qhomographic_sg_denom_nonzero. replace Zero with (Z_to_Q 0); trivial. rewrite H. rewrite Qmult_one_right. rewrite <- Z_to_Qplus. apply Z_to_Q_not_eq. assumption. rewrite Qpos_nR. replace (Qplus (Qmult c (Qplus (Qpos xs) Qone)) d) with (Qplus (Qmult c (Qpos xs)) (Qplus c d)). rewrite <- Z_to_Qplus. assumption. abstract ring. rewrite Qpos_dL. replace (Qplus (Qmult c (Qmult (Qpos xs) (Qinv (Qplus (Qpos xs) Qone)))) d) with (Qmult (Qplus (Qmult (Qplus c d) (Qpos xs)) d) (Qinv (Qplus (Qpos xs) Qone))). apply Qmult_resp_nonzero. rewrite <- Z_to_Qplus. assumption. abstract discriminate. abstract (field; discriminate). Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)