proposition: Lemma Qquadratic_sg_denom_nonzero_correct_1 : forall (e f g h : Z) (p1 p2 : Qpositive), Qquadratic_sg_denom_nonzero e f g h p1 p2 -> Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos p1)) (Qpos p2)) (Qmult f (Qpos p1))) (Qmult g (Qpos p2))) h <> Zero.
proof: Proof. intros e f g h p1 p2 H_Qquadratic_sg_denom_nonzero. induction H_Qquadratic_sg_denom_nonzero. replace Zero with (Z_to_Q 0); trivial. rewrite H. repeat rewrite Qmult_one_right. rewrite <- Q_distr_left. rewrite <- Qplus_assoc. do 2 rewrite <- Z_to_Qplus. apply Qhomographic_sg_denom_nonzero_correct_1; assumption. replace Zero with (Z_to_Q 0); trivial. rewrite H. repeat rewrite Qmult_one_right. rewrite <- Qplus_assoc with (m := Z_to_Q f). rewrite (Qplus_sym f). rewrite Qplus_assoc. rewrite <- Q_distr_left. rewrite <- Qplus_assoc. do 2 rewrite <- Z_to_Qplus. apply Qhomographic_sg_denom_nonzero_correct_1; assumption. do 2 rewrite Qpos_nR. intro H. apply IHH_Qquadratic_sg_denom_nonzero. rewrite <- H. repeat rewrite Z_to_Qplus. abstract ring. abstract (rewrite Qpos_nR; rewrite Qpos_dL; intro H; repeat rewrite Z_to_Qplus in IHH_Qquadratic_sg_denom_nonzero; apply (Qmult_resp_nonzero _ (Qinv (Qplus (Qpos p2) Qone)) IHH_Qquadratic_sg_denom_nonzero); [ discriminate | rewrite <- H; field; discriminate ]). abstract (rewrite Qpos_nR; rewrite Qpos_dL; intro H; repeat rewrite Z_to_Qplus in IHH_Qquadratic_sg_denom_nonzero; apply (Qmult_resp_nonzero _ (Qinv (Qplus (Qpos p1) Qone)) IHH_Qquadratic_sg_denom_nonzero); [ discriminate | rewrite <- H; field; discriminate ]). abstract (do 2 rewrite Qpos_dL; intro H; repeat rewrite Z_to_Qplus in IHH_Qquadratic_sg_denom_nonzero; apply (Qmult_resp_nonzero _ (Qinv (Qmult (Qplus (Qpos p1) Qone) (Qplus (Qpos p2) Qone))) IHH_Qquadratic_sg_denom_nonzero); [ discriminate | rewrite <- H; field; split; discriminate ]). Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)