proposition: Lemma Qquadratic_denom_nonzero_correct_1 : forall (e f g h : Z) (q1 q2 : Q), Qquadratic_denom_nonzero e f g h q1 q2 -> Qplus (Qplus (Qplus (Qmult (Qmult e q1) q2) (Qmult f q1)) (Qmult g q2)) h <> Zero.
proof: Proof. intros e f g h q1 q2 H_Qquadratic_denom_nonzero; induction H_Qquadratic_denom_nonzero. rewrite H. rewrite H0. repeat rewrite Qmult_zero_right. repeat rewrite Qplus_zero_left. change (Z_to_Q h <> Z_to_Q 0) in |- *. apply Z_to_Q_not_eq; assumption. rewrite H. repeat rewrite Qmult_zero_right. repeat rewrite Qplus_zero_left. rewrite H0. apply Qhomographic_sg_denom_nonzero_correct_1; assumption. rewrite H. repeat rewrite Qmult_zero_right. repeat rewrite Qplus_zero_left. rewrite H0. rewrite Qopp_Qpos. generalize (Qhomographic_sg_denom_nonzero_correct_1 _ _ _ H1). intros H' H2; apply H'. rewrite <- H2. rewrite Z_to_Qopp. abstract ring. rewrite H. rewrite H0. repeat rewrite Qmult_zero_right. rewrite Qplus_zero_left. rewrite Qplus_zero_right. apply Qhomographic_sg_denom_nonzero_correct_1; assumption. rewrite H. rewrite H0. repeat rewrite Qmult_zero_right. rewrite Qplus_zero_left. rewrite Qplus_zero_right. rewrite Qopp_Qpos. generalize (Qhomographic_sg_denom_nonzero_correct_1 _ _ _ H1). intros H' H2; apply H'. rewrite <- H2. rewrite Z_to_Qopp. abstract ring. rewrite H. rewrite H0. apply Qquadratic_sg_denom_nonzero_correct_1; assumption. rewrite H. rewrite H0. generalize (Qquadratic_sg_denom_nonzero_correct_1 _ _ _ _ _ _ H1). intros H' H2; apply H'. rewrite <- H2. repeat rewrite Z_to_Qopp. repeat rewrite Qopp_Qpos. abstract ring. rewrite H. rewrite H0. generalize (Qquadratic_sg_denom_nonzero_correct_1 _ _ _ _ _ _ H1). intros H' H2; apply H'. rewrite <- H2. repeat rewrite Z_to_Qopp. repeat rewrite Qopp_Qpos. abstract ring. rewrite H. rewrite H0. generalize (Qquadratic_sg_denom_nonzero_correct_1 _ _ _ _ _ _ H1). intros H' H2; apply H'. rewrite <- H2. repeat rewrite Z_to_Qopp. repeat rewrite Qopp_Qpos. abstract ring. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)