proposition: Lemma quadratic_output_bit : forall (a b c d e f g h : Z) (p1 p2 : Qpositive) (hyp_quadraticAcc : quadraticAcc a b c d e f g h p1 p2), Qquadratic_Qpositive_to_Qpositive a b c d e f g h p1 p2 hyp_quadraticAcc = spec_Qquadratic_Qpositive_to_Qpositive2 a b c d e f g h p1 p2.
proof: Proof. intros a b c d e f g h p1 p2 hyp_quadraticAcc. generalize (quadraticAcc_positive_numerator _ _ _ _ _ _ _ _ _ _ hyp_quadraticAcc). generalize (quadraticAcc_positive_denominator _ _ _ _ _ _ _ _ _ _ hyp_quadraticAcc). pattern a, b, c, d, e, f, g, h, p1, p2, hyp_quadraticAcc in |- *. elim hyp_quadraticAcc using quadraticAcc_ind_dep; clear a b c d e f g h p1 p2 hyp_quadraticAcc; intros; unfold Qquadratic_Qpositive_to_Qpositive;fold Qquadratic_Qpositive_to_Qpositive. case (Qpositive_dec_One p1); intros Hp1; [ idtac | Falsum ]. unfold spec_Qquadratic_Qpositive_to_Qpositive2 in |- *. rewrite output_bit. unfold spec_ni2 in |- *. rewrite e0. repeat rewrite Qmult_one_right. apply f_equal2 with Qpositive Qpositive; try apply f_equal with Qpositive; apply f_equal with Q; repeat rewrite Z_to_Qplus; abstract ring. case (Qpositive_dec_One p1); intros Hp1; [ Falsum | idtac ]; case (Qpositive_dec_One p2); intros Hp2; [ idtac | Falsum ]. unfold spec_Qquadratic_Qpositive_to_Qpositive2 in |- *. rewrite output_bit. unfold spec_ni2 in |- *. rewrite e0. repeat rewrite Qmult_one_right. apply f_equal2 with Qpositive Qpositive; try apply f_equal with Qpositive; apply f_equal with Q; repeat rewrite Z_to_Qplus; abstract ring. case (Qpositive_dec_One p1); intros Hp1; [ Falsum | idtac ]; case (Qpositive_dec_One p2); intros Hp2; [ Falsum | idtac ]; case (quadratic_top_more_informative a b c d e f g h); intros Habcdefgh; [ idtac | Falsum ]; generalize (quadraticAcc_positive_numerator _ _ _ _ _ _ _ _ _ _ q0); intros H_ae;simpl; rewrite H; try assumption; apply spec_Qquadratic_Qpositive_to_Qpositive2_nR_emission; assumption. case (Qpositive_dec_One p1); intros Hp1; [ Falsum | idtac ]; case (Qpositive_dec_One p2); intros Hp2; [ Falsum | idtac ]; case (quadratic_top_more_informative a b c d e f g h); intros Habcdefgh; [ Falsum | idtac ]; case (quadratic_top_more_informative e f g h a b c d); intros Hefghabcd; [ idtac | Falsum ]; generalize (quadraticAcc_positive_denominator _ _ _ _ _ _ _ _ _ _ q0); intros H_ae; simpl;rewrite H; try assumption; apply spec_Qquadratic_Qpositive_to_Qpositive2_dL_emission; assumption. case (quadratic_top_more_informative a b c d e f g h); intros Habcdefgh; [ Falsum | idtac ]; case (quadratic_top_more_informative e f g h a b c d); intros Hefghabcd; [ Falsum | idtac ]; generalize (quadraticAcc_positive_numerator _ _ _ _ _ _ _ _ _ _ q); generalize (quadraticAcc_positive_denominator _ _ _ _ _ _ _ _ _ _ q); intros H_ae H_ae'; simpl; rewrite H; try assumption; rewrite spec_Qquadratic_Qpositive_to_Qpositive2_nR_nR; reflexivity. case (quadratic_top_more_informative a b c d e f g h); intros Habcdefgh; [ Falsum | idtac ]; case (quadratic_top_more_informative e f g h a b c d); intros Hefghabcd; [ Falsum | idtac ]; generalize (quadraticAcc_positive_numerator _ _ _ _ _ _ _ _ _ _ q); generalize (quadraticAcc_positive_denominator _ _ _ _ _ _ _ _ _ _ q); intros H_ae H_ae'; simpl;rewrite H; try assumption; rewrite spec_Qquadratic_Qpositive_to_Qpositive2_nR_dL; reflexivity || apply Qlt_not_eq; repeat rewrite <- Z_to_Qplus; assumption. case (quadratic_top_more_informative a b c d e f g h); intros Habcdefgh; [ Falsum | idtac ]; case (quadratic_top_more_informative e f g h a b c d); intros Hefghabcd; [ Falsum | idtac ]; generalize (quadraticAcc_positive_numerator _ _ _ _ _ _ _ _ _ _ q); generalize (quadraticAcc_positive_denominator _ _ _ _ _ _ _ _ _ _ q); intros H_ae H_ae'; simpl;rewrite H; try assumption; rewrite spec_Qquadratic_Qpositive_to_Qpositive2_dL_nR; reflexivity || apply Qlt_not_eq; repeat rewrite <- Z_to_Qplus; assumption. case (quadratic_top_more_informative a b c d e f g h); intros Habcdefgh; [ Falsum | idtac ]; case (quadratic_top_more_informative e f g h a b c d); intros Hefghabcd; [ Falsum | idtac ]; generalize (quadraticAcc_positive_numerator _ _ _ _ _ _ _ _ _ _ q); generalize (quadraticAcc_positive_denominator _ _ _ _ _ _ _ _ _ _ q); intros H_ae H_ae'; simpl; rewrite H; try assumption; rewrite spec_Qquadratic_Qpositive_to_Qpositive2_dL_dL; reflexivity || apply Qlt_not_eq; repeat rewrite <- Z_to_Qplus; assumption. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)