proposition: Lemma Qquadratic_sg_denom_nonzero_correct_2 : forall (e f g h : Z) (p1 p2 : Qpositive), Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos p1)) (Qpos p2)) (Qmult f (Qpos p1))) (Qmult g (Qpos p2))) h <> Zero -> Qquadratic_sg_denom_nonzero e f g h p1 p2.
proof: Proof. intros e f g h p1. generalize e f g h. clear e f g h. induction p1 as [xs| xs| ]. intros e f g h p2. generalize e f g h; clear e f g h. destruct p2 as [ys| ys| ]. intros e f g h H. apply Qquadratic_signok1. apply IHxs. intro H'; apply H. do 2 rewrite Qpos_nR. rewrite <- H'. repeat rewrite Z_to_Qplus. abstract ring. intros e f g h H. apply Qquadratic_signok2. apply IHxs. repeat rewrite Z_to_Qplus. repeat rewrite Qpos_dL in H; repeat rewrite Qpos_nR in H. assert (H0 : Qplus (Qpos ys) Qone <> Zero); [ discriminate | idtac ]. generalize (Qmult_resp_nonzero _ (Qplus (Qpos ys) Qone) H H0). intro H1. intro H'. apply H1. rewrite <- H'. abstract (field; discriminate). intros e f g h H. apply Qquadratic_signok0. reflexivity. apply Qhomographic_sg_denom_nonzero_correct_2. do 2 rewrite Z_to_Qplus. intro H'; apply H. rewrite <- H'. abstract ring. intros e f g h p2. generalize e f g h; clear e f g h. destruct p2 as [ys| ys| ]. intros e f g h H. apply Qquadratic_signok3. apply IHxs. repeat rewrite Z_to_Qplus. repeat rewrite Qpos_dL in H; repeat rewrite Qpos_nR in H. assert (H0 : Qplus (Qpos xs) Qone <> Zero); [ discriminate | idtac ]. generalize (Qmult_resp_nonzero _ (Qplus (Qpos xs) Qone) H H0). intro H1. intro H'. apply H1. rewrite <- H'. abstract (field; discriminate). intros e f g h H. apply Qquadratic_signok4. apply IHxs. repeat rewrite Z_to_Qplus. repeat rewrite Qpos_dL in H. assert (H0 : Qmult (Qplus (Qpos xs) Qone) (Qplus (Qpos ys) Qone) <> Zero); [ discriminate | idtac ]. generalize (Qmult_resp_nonzero _ (Qmult (Qplus (Qpos xs) Qone) (Qplus (Qpos ys) Qone)) H H0). intro H1. intro H'. apply H1. rewrite <- H'. abstract (field; split; discriminate). intros e f g h H. apply Qquadratic_signok0. reflexivity. apply Qhomographic_sg_denom_nonzero_correct_2. do 2 rewrite Z_to_Qplus. intro H'; apply H. rewrite <- H'. abstract ring. intros e f g h p2 H. apply Qquadratic_signok0'. reflexivity. apply Qhomographic_sg_denom_nonzero_correct_2. do 2 rewrite Z_to_Qplus. intro H'; apply H. rewrite <- H'. abstract ring. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)