proposition: Lemma Qquadratic_denom_nonzero_correct_2 : forall (e f g h : Z) (q1 q2 : Q), Qplus (Qplus (Qplus (Qmult (Qmult e q1) q2) (Qmult f q1)) (Qmult g q2)) h <> Zero -> Qquadratic_denom_nonzero e f g h q1 q2.
proof: Proof. intros e f g h [| p1| p1] [| p2| p2] H_denom. apply Qquadraticok00; trivial. intro H. apply H_denom. rewrite H. simpl in |- *. abstract ring. apply Qquadraticok01 with p2; trivial. apply Qhomographic_sg_denom_nonzero_correct_2. intro H. apply H_denom. repeat rewrite Qmult_zero_right. rewrite Qmult_zero. repeat rewrite Qplus_zero_left. assumption. apply Qquadraticok02 with p2; trivial. apply Qhomographic_sg_denom_nonzero_correct_2. intro H. apply H_denom. repeat rewrite Qmult_zero_right. rewrite Qmult_zero. repeat rewrite Qplus_zero_left. rewrite <- Qmult_neg in H. rewrite Z_to_Qopp in H. rewrite Qmult_Qopp_left in H. rewrite <- H. abstract ring. apply Qquadraticok10 with p1; trivial. apply Qhomographic_sg_denom_nonzero_correct_2. intro H. apply H_denom. repeat rewrite Qmult_zero_right. repeat rewrite Qplus_zero_left. repeat rewrite Qplus_zero_right. assumption. apply Qquadraticok11 with p1 p2; trivial. apply Qquadratic_sg_denom_nonzero_correct_2. assumption. apply Qquadraticok12 with p1 p2; trivial. apply Qquadratic_sg_denom_nonzero_correct_2. repeat rewrite Z_to_Qopp. repeat rewrite <- Qmult_neg. intro H. apply H_denom. repeat rewrite <- Qmult_neg. rewrite <- H. abstract ring. apply Qquadraticok20 with p1; trivial. apply Qhomographic_sg_denom_nonzero_correct_2. intro H. apply H_denom. repeat rewrite Qmult_zero_right. rewrite Qplus_zero_left. rewrite Qplus_zero_right. rewrite <- Qmult_neg in H. rewrite Z_to_Qopp in H. rewrite <- H. abstract ring. apply Qquadraticok21 with p1 p2; trivial. apply Qquadratic_sg_denom_nonzero_correct_2. repeat rewrite Z_to_Qopp. repeat rewrite <- Qmult_neg. intro H. apply H_denom. repeat rewrite <- Qmult_neg. rewrite <- H. abstract ring. apply Qquadraticok22 with p1 p2; trivial. apply Qquadratic_sg_denom_nonzero_correct_2. repeat rewrite Z_to_Qopp. repeat rewrite <- Qmult_neg. intro H. apply H_denom. repeat rewrite <- Qmult_neg. rewrite <- H. abstract ring. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)