proposition: Lemma Qquadratic_Qpositive_to_Qpositive_equal : forall (a b c d e f g h : Z) (p1 p2 : Qpositive) (hyp1 hyp2 : 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 hyp1 = Qquadratic_Qpositive_to_Qpositive a b c d e f g h p1 p2 hyp2.
proof: Proof. intros a b c d e f g h p1 p2 hyp1. pattern a, b, c, d, e, f, g, h, p1, p2, hyp1 in |- *. elim hyp1 using quadraticAcc_ind_dep; clear a b c d e f g h p1 p2 hyp1. intros a b c d e f g h p1 p2 Hp1 hAcc hyp2; generalize Hp1 hAcc; clear Hp1 hAcc. pattern a, b, c, d, e, f, g, h, p1, p2, hyp2 in |- *. elim hyp2 using quadraticAcc_ind_dep; clear a b c d e f g h p1 p2 hyp2; intros. unfold Qquadratic_Qpositive_to_Qpositive;fold Qquadratic_Qpositive_to_Qpositive; case (Qpositive_dec_One p1); intros Hp; [ idtac | Falsum ]; apply Qhomographic_Qpositive_to_Qpositive_equal. Falsum. Falsum. Falsum. discriminate Hp1. discriminate Hp1. discriminate Hp1. discriminate Hp1. intros a b c d e f g h p1 p2 Hp1 Hp2 hAcc hyp2; generalize Hp1 Hp2 hAcc; clear Hp1 Hp2 hAcc. pattern a, b, c, d, e, f, g, h, p1, p2, hyp2 in |- *. elim hyp2 using quadraticAcc_ind_dep; clear a b c d e f g h p1 p2 hyp2; intros. Falsum. unfold Qquadratic_Qpositive_to_Qpositive;fold Qquadratic_Qpositive_to_Qpositive; case (Qpositive_dec_One p1); intros Hp1_; [ Falsum | idtac ]; case (Qpositive_dec_One p2); intros Hp2_; [ idtac | Falsum ]; apply Qhomographic_Qpositive_to_Qpositive_equal. Falsum. Falsum. discriminate Hp2. discriminate Hp2. discriminate Hp2. discriminate Hp2. intros a b c d e f g h p1 p2 Hp1 Hp2 Habcdefgh qAcc H_ind hyp2. generalize Hp1 Hp2 Habcdefgh qAcc H_ind; clear Hp1 Hp2 Habcdefgh qAcc H_ind. pattern a, b, c, d, e, f, g, h, p1, p2, hyp2 in |- *. elim hyp2 using quadraticAcc_ind_dep; clear a b c d e f g h p1 p2 hyp2; intros. Falsum. Falsum. unfold Qquadratic_Qpositive_to_Qpositive;fold Qquadratic_Qpositive_to_Qpositive; 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 ]; apply f_equal with Qpositive; apply H_ind. Falsum. Falsum. Falsum. Falsum. Falsum. intros a b c d e f g h p1 p2 Hp1 Hp2 Habcdefgh Hefghabcd qAcc H_ind hyp2. generalize Hp1 Hp2 Habcdefgh Hefghabcd qAcc H_ind; clear Hp1 Hp2 Habcdefgh Hefghabcd qAcc H_ind. pattern a, b, c, d, e, f, g, h, p1, p2, hyp2 in |- *. elim hyp2 using quadraticAcc_ind_dep; clear a b c d e f g h p1 p2 hyp2; intros; try solve [ Falsum ]. unfold Qquadratic_Qpositive_to_Qpositive;fold Qquadratic_Qpositive_to_Qpositive; 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 ]; apply f_equal with Qpositive; apply H_ind. intros a b c d e f g h xs ys Habcdefgh Hefghabcd qAcc H_ind hyp2. set (P1 := nR xs) in *; assert (HP1 : P1 = nR xs); trivial; generalize HP1. set (P2 := nR ys) in *; assert (HP2 : P2 = nR ys); trivial; generalize HP2. generalize Habcdefgh Hefghabcd qAcc H_ind; clear Habcdefgh Hefghabcd qAcc H_ind. elim hyp2 using quadraticAcc_ind_dep with (P := fun (a b c d e f g h : Z) (P1 P2 : Qpositive) (hyp2 : quadraticAcc a b c d e f g h P1 P2) => forall (Habcdefgh : ~ quadratic_top_more a b c d e f g h) (Hefghabcd : ~ quadratic_top_more e f g h a b c d) (qAcc : quadraticAcc a (a + b) (a + c) (a + b + c + d) e (e + f) (e + g) (e + f + g + h) xs ys), (forall hyp2 : quadraticAcc a (a + b) (a + c) (a + b + c + d) e (e + f) (e + g) (e + f + g + h) xs ys, Qquadratic_Qpositive_to_Qpositive a (a + b) (a + c) (a + b + c + d) e (e + f) (e + g) (e + f + g + h) xs ys qAcc = Qquadratic_Qpositive_to_Qpositive a (a + b) (a + c) (a + b + c + d) e (e + f) (e + g) (e + f + g + h) xs ys hyp2) -> P2 = nR ys -> P1 = nR xs -> Qquadratic_Qpositive_to_Qpositive a b c d e f g h (nR xs) (nR ys) (quadraticacc3_II a b c d e f g h xs ys Habcdefgh Hefghabcd qAcc) = Qquadratic_Qpositive_to_Qpositive a b c d e f g h P1 P2 hyp2); clear a b c d e f g h hyp2; intros. Falsum; rewrite H1 in e0; discriminate e0. Falsum; rewrite H0 in e0; discriminate e0. Falsum. Falsum. unfold Qquadratic_Qpositive_to_Qpositive;fold Qquadratic_Qpositive_to_Qpositive; 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 q; let T_local1 := eval compute in (f_equal Qpositive_tail H1) in let T_local2 := eval compute in (f_equal Qpositive_tail H2) in (rewrite T_local1; rewrite T_local2; apply H0). discriminate H1. discriminate H2. discriminate H1. intros a b c d e f g h xs ys Habcdefgh Hefghabcd qAcc H_ind hyp2. set (P1 := nR xs) in *; assert (HP1 : P1 = nR xs); trivial; generalize HP1. set (P2 := dL ys) in *; assert (HP2 : P2 = dL ys); trivial; generalize HP2. generalize Habcdefgh Hefghabcd qAcc H_ind; clear Habcdefgh Hefghabcd qAcc H_ind. elim hyp2 using quadraticAcc_ind_dep with (P := fun (a b c d e f g h : Z) (P1 P2 : Qpositive) (hyp2 : quadraticAcc a b c d e f g h P1 P2) => forall (Habcdefgh : ~ quadratic_top_more a b c d e f g h) (Hefghabcd : ~ quadratic_top_more e f g h a b c d) (qAcc : quadraticAcc (a + b) b (a + b + c + d) (b + d) (e + f) f (e + f + g + h) (f + h) xs ys), (forall hyp2 : quadraticAcc (a + b) b (a + b + c + d) (b + d) (e + f) f (e + f + g + h) (f + h) xs ys, Qquadratic_Qpositive_to_Qpositive (a + b) b (a + b + c + d) (b + d) (e + f) f (e + f + g + h) (f + h) xs ys qAcc = Qquadratic_Qpositive_to_Qpositive (a + b) b (a + b + c + d) (b + d) (e + f) f (e + f + g + h) (f + h) xs ys hyp2) -> P2 = dL ys -> P1 = nR xs -> Qquadratic_Qpositive_to_Qpositive a b c d e f g h (nR xs) (dL ys) (quadraticacc3_IO a b c d e f g h xs ys Habcdefgh Hefghabcd qAcc) = Qquadratic_Qpositive_to_Qpositive a b c d e f g h P1 P2 hyp2); clear a b c d e f g h hyp2; intros. Falsum; rewrite H1 in e0; discriminate e0. Falsum; rewrite H0 in e0; discriminate e0. Falsum. Falsum. discriminate H1. unfold Qquadratic_Qpositive_to_Qpositive;fold Qquadratic_Qpositive_to_Qpositive; 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 q; let T_local1 := eval compute in (f_equal Qpositive_tail H1) in let T_local2 := eval compute in (f_equal Qpositive_tail H2) in (rewrite T_local1; rewrite T_local2; apply H0). discriminate H2. discriminate H2. intros a b c d e f g h xs ys Habcdefgh Hefghabcd qAcc H_ind hyp2. set (P1 := dL xs) in *; assert (HP1 : P1 = dL xs); trivial; generalize HP1. set (P2 := nR ys) in *; assert (HP2 : P2 = nR ys); trivial; generalize HP2. generalize Habcdefgh Hefghabcd qAcc H_ind; clear Habcdefgh Hefghabcd qAcc H_ind. elim hyp2 using quadraticAcc_ind_dep with (P := fun (a b c d e f g h : Z) (P1 P2 : Qpositive) (hyp2 : quadraticAcc a b c d e f g h P1 P2) => forall (Habcdefgh : ~ quadratic_top_more a b c d e f g h) (Hefghabcd : ~ quadratic_top_more e f g h a b c d) (qAcc : quadraticAcc (a + c) (a + b + c + d) c (c + d) (e + g) (e + f + g + h) g (g + h) xs ys), (forall hyp2 : quadraticAcc (a + c) (a + b + c + d) c (c + d) (e + g) (e + f + g + h) g (g + h) xs ys, Qquadratic_Qpositive_to_Qpositive (a + c) (a + b + c + d) c (c + d) (e + g) (e + f + g + h) g (g + h) xs ys qAcc = Qquadratic_Qpositive_to_Qpositive (a + c) (a + b + c + d) c (c + d) (e + g) (e + f + g + h) g (g + h) xs ys hyp2) -> P2 = nR ys -> P1 = dL xs -> Qquadratic_Qpositive_to_Qpositive a b c d e f g h (dL xs) (nR ys) (quadraticacc3_OI a b c d e f g h xs ys Habcdefgh Hefghabcd qAcc) = Qquadratic_Qpositive_to_Qpositive a b c d e f g h P1 P2 hyp2); clear a b c d e f g h hyp2; intros. Falsum; rewrite H1 in e0; discriminate e0. Falsum; rewrite H0 in e0; discriminate e0. Falsum. Falsum. discriminate H2. discriminate H1. unfold Qquadratic_Qpositive_to_Qpositive;fold Qquadratic_Qpositive_to_Qpositive; 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 q; let T_local1 := eval compute in (f_equal Qpositive_tail H1) in let T_local2 := eval compute in (f_equal Qpositive_tail H2) in (rewrite T_local1; rewrite T_local2; apply H0). discriminate H1. intros a b c d e f g h xs ys Habcdefgh Hefghabcd qAcc H_ind hyp2. set (P1 := dL xs) in *; assert (HP1 : P1 = dL xs); trivial; generalize HP1. set (P2 := dL ys) in *; assert (HP2 : P2 = dL ys); trivial; generalize HP2. generalize Habcdefgh Hefghabcd qAcc H_ind; clear Habcdefgh Hefghabcd qAcc H_ind. elim hyp2 using quadraticAcc_ind_dep with (P := fun (a b c d e f g h : Z) (P1 P2 : Qpositive) (hyp2 : quadraticAcc a b c d e f g h P1 P2) => forall (Habcdefgh : ~ quadratic_top_more a b c d e f g h) (Hefghabcd : ~ quadratic_top_more e f g h a b c d) (qAcc : quadraticAcc (a + b + c + d) (b + d) (c + d) d (e + f + g + h) (f + h) (g + h) h xs ys), (forall hyp2 : quadraticAcc (a + b + c + d) (b + d) (c + d) d (e + f + g + h) (f + h) (g + h) h xs ys, Qquadratic_Qpositive_to_Qpositive (a + b + c + d) (b + d) (c + d) d (e + f + g + h) (f + h) (g + h) h xs ys qAcc = Qquadratic_Qpositive_to_Qpositive (a + b + c + d) (b + d) (c + d) d (e + f + g + h) (f + h) (g + h) h xs ys hyp2) -> P2 = dL ys -> P1 = dL xs -> Qquadratic_Qpositive_to_Qpositive a b c d e f g h (dL xs) (dL ys) (quadraticacc3_OO a b c d e f g h xs ys Habcdefgh Hefghabcd qAcc) = Qquadratic_Qpositive_to_Qpositive a b c d e f g h P1 P2 hyp2); clear a b c d e f g h hyp2; intros. Falsum; rewrite H1 in e0; discriminate e0. Falsum; rewrite H0 in e0; discriminate e0. Falsum. Falsum. discriminate H2. discriminate H2. discriminate H1. unfold Qquadratic_Qpositive_to_Qpositive;fold Qquadratic_Qpositive_to_Qpositive; 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 q; let T_local1 := eval compute in (f_equal Qpositive_tail H1) in let T_local2 := eval compute in (f_equal Qpositive_tail H2) in (rewrite T_local1; rewrite T_local2; apply H0). Qed.
imports: QArithSternBrocot(Merge_Order)