proposition: Lemma Qhomographic_sg_denom_nonzero_correct_2 : forall (c d : Z) (p : Qpositive), Qplus (Qmult c (Qpos p)) d <> Zero -> Qhomographic_sg_denom_nonzero c d p.
proof: Proof. intros c d p. generalize c d. clear c d. induction p. intros. apply Qhomographic_signok1. apply IHp. replace (Qplus (Qmult c (Qpos p)) (c + d)%Z) with (Qplus (Qmult c (Qplus (Qpos p) Qone)) d). rewrite Qpos_nR in H; assumption. rewrite Z_to_Qplus. abstract ring. intros. apply Qhomographic_signok2. apply IHp. intro. apply H. rewrite Qpos_dL. replace (Qplus (Qmult c (Qmult (Qpos p) (Qinv (Qplus (Qpos p) Qone)))) d) with (Qmult (Qplus (Qmult (Qplus c d) (Qpos p)) d) (Qinv (Qplus (Qpos p) Qone))). rewrite <- Z_to_Qplus. rewrite H0. rewrite Qmult_zero; reflexivity. abstract (field; discriminate). intros. apply Qhomographic_signok0; trivial. intro. apply H. rewrite Qmult_one_right. rewrite <- Z_to_Qplus. replace Zero with (Z_to_Q 0); trivial. apply f_equal with Z; assumption. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)