proposition: Lemma quadratic : forall (a b c d e f g h : Z) (s1 s2 : Q) (H_Qquadratic_denom_nonzero : Qquadratic_denom_nonzero e f g h s1 s2), Qquadratic a b c d e f g h s1 s2 H_Qquadratic_denom_nonzero = spec_q a b c d e f g h s1 s2.
proof: Proof. intros a b c d e f g h [| p1| p1] [| p2| p2] H_Qhomographic_denom_nonzero. unfold Qquadratic in |- *. rewrite homography. unfold spec_q, spec_h in |- *. repeat rewrite Qmult_zero_right. repeat rewrite Qplus_zero_left. reflexivity. unfold Qquadratic in |- *. rewrite homography. unfold spec_q, spec_h in |- *. repeat rewrite Qmult_zero_right. repeat rewrite Qplus_zero_left. reflexivity. unfold Qquadratic in |- *. rewrite homography. unfold spec_q, spec_h in |- *. repeat rewrite Qmult_zero_right. repeat rewrite Qplus_zero_left. reflexivity. unfold Qquadratic in |- *. rewrite homography. unfold spec_q, spec_h in |- *. repeat rewrite Qmult_zero_right. repeat rewrite Qplus_zero_right. repeat rewrite Qplus_zero_left. reflexivity. unfold Qquadratic in |- *. unfold spec_q in |- *. apply quadratic_positive_input. unfold Qquadratic in |- *. unfold spec_q in |- *. rewrite quadratic_positive_input. apply f_equal2 with Q Q; [ idtac | apply f_equal with Q ]; apply f_equal2 with Q Q; trivial; repeat rewrite Z_to_Qopp; repeat rewrite <- Qmult_neg; abstract ring. unfold Qquadratic in |- *. rewrite homography. unfold spec_q, spec_h in |- *. repeat rewrite Qmult_zero_right. repeat rewrite Qplus_zero_right. repeat rewrite Qplus_zero_left. reflexivity. unfold Qquadratic in |- *. unfold spec_q in |- *. rewrite quadratic_positive_input. apply f_equal2 with Q Q; [ idtac | apply f_equal with Q ]; apply f_equal2 with Q Q; trivial; repeat rewrite Z_to_Qopp; repeat rewrite <- Qmult_neg; abstract ring. unfold Qquadratic in |- *. unfold spec_q in |- *. rewrite quadratic_positive_input. apply f_equal2 with Q Q; [ idtac | apply f_equal with Q ]; apply f_equal2 with Q Q; trivial; repeat rewrite Z_to_Qopp; repeat rewrite <- Qmult_neg; abstract ring. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)