proposition: Lemma quadratic_positive_input : forall (a b c d e f g h : Z) (p1 p2 : Qpositive) (H_Qquadratic_sg_denom_nonzero : Qquadratic_sg_denom_nonzero e f g h p1 p2), Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero = Qmult (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos p1)) (Qpos p2)) (Qmult b (Qpos p1))) (Qmult c (Qpos p2))) d) (Qinv (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos p1)) (Qpos p2)) (Qmult f (Qpos p1))) (Qmult g (Qpos p2))) h)).
proof: Proof. intros a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero. functional induction (Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero); Clear_eq_. rewrite coding_Q. unfold spec_fraction_encoding in |- *. generalize s; intros (H1, (H2, (H3, (H4, (H5, H6))))); repeat match goal with | id1:(_ = _ :>Z) |- _ => generalize (f_equal Z_to_Q id1); clear id1; intro id1; do 2 rewrite Z_to_Qmult in id1 end. apply a_field_equality_2; [ replace Zero with (Z_to_Q 0); trivial; apply Z_to_Q_not_eq; assumption | assumption | assumption | assumption | apply Qquadratic_sg_denom_nonzero_correct_1; assumption ]. rewrite coding_Q. unfold spec_fraction_encoding in |- *. generalize s; intros (H1, (H2, (H3, (H4, (H5, H6))))); repeat match goal with | id1:(_ = _ :>Z) |- _ => generalize (f_equal Z_to_Q id1); clear id1; intro id1; do 2 rewrite Z_to_Qmult in id1 end. apply a_field_equality_3; [ replace Zero with (Z_to_Q 0); trivial; apply Z_to_Q_not_eq; assumption | assumption | assumption | assumption | apply Qquadratic_sg_denom_nonzero_correct_1; assumption ]. rewrite coding_Q. unfold spec_fraction_encoding in |- *. generalize s; intros (H1, (H2, (H3, (H4, (H5, H6))))); repeat match goal with | id1:(_ = _ :>Z) |- _ => generalize (f_equal Z_to_Q id1); clear id1; intro id1; do 2 rewrite Z_to_Qmult in id1 end. apply a_field_equality_4; [ replace Zero with (Z_to_Q 0); trivial; apply Z_to_Q_not_eq; assumption | assumption | assumption | assumption | apply Qquadratic_sg_denom_nonzero_correct_1; assumption ]. rewrite coding_Q. unfold spec_fraction_encoding in |- *. generalize s; intros (H1, (H2, (H3, (H4, (H5, H6))))); repeat match goal with | id1:(_ = _ :>Z) |- _ => generalize (f_equal Z_to_Q id1); clear id1; intro id1; do 2 rewrite Z_to_Qmult in id1 end. apply a_field_equality_5; [ replace Zero with (Z_to_Q 0); trivial; apply Z_to_Q_not_eq; assumption | assumption | assumption | assumption | apply Qquadratic_sg_denom_nonzero_correct_1; assumption ]. transitivity (spec_Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2); trivial; symmetry in |- *; apply Qsgn_2; rewrite <- (quadratic_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) ; assumption. Absurd_q_sign_. rewrite quadratic_output_bit; rewrite <- spec_Qquadratic_Qpositive_to_Q_spec_Qquadratic_Qpositive_to_Qpositive2_pos ; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qquadratic_sign_pres_fraction; [ reflexivity | change (Qsgn (spec_Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2) = 1%Z) in |- *; rewrite <- (quadratic_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) ; assumption ]. rewrite quadratic_output_bit; rewrite <- spec_Qquadratic_Qpositive_to_Q_spec_Qquadratic_Qpositive_to_Qpositive2_pos ; rewrite spec_Qquadratic_Qpositive_to_Q_Zopp; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qquadratic_sign_pres_fraction; [ reflexivity | change (Qsgn (spec_Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2) = 1%Z) in |- *; rewrite <- (quadratic_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) ; assumption ]. Absurd_q_sign_. rewrite quadratic_output_bit; rewrite <- spec_Qquadratic_Qpositive_to_Q_spec_Qquadratic_Qpositive_to_Qpositive2_neg_2 ; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qquadratic_sign_pres_fraction; [ reflexivity | change (Qsgn (spec_Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2) = (-1)%Z) in |- *; rewrite <- (quadratic_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) ; assumption ]. rewrite quadratic_output_bit; rewrite <- spec_Qquadratic_Qpositive_to_Q_spec_Qquadratic_Qpositive_to_Qpositive2_neg_1 ; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qquadratic_sign_pres_fraction; [ reflexivity | change (Qsgn (spec_Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2) = (-1)%Z) in |- *; rewrite <- (quadratic_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) ; assumption ]. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)