proposition: Lemma quadraticAcc_wf : forall (a b c d e f g h : Z) (p1 p2 : Qpositive), (0 < a + b + c + d)%Z -> (0 < e + f + g + h)%Z -> (0 <= a)%Z -> (0 <= b)%Z -> (0 <= c)%Z -> (0 <= d)%Z -> (0 <= e)%Z -> (0 <= f)%Z -> (0 <= g)%Z -> (0 <= h)%Z -> quadraticAcc a b c d e f g h p1 p2.
proof: Proof. intros a b c d e f g h p1 p2 Habcd Hefgh Ha Hb Hc Hd He Hf Hg Hh. set (pos_a := Build_Z_pos a Ha) in *. set (pos_b := Build_Z_pos b Hb) in *. set (pos_c := Build_Z_pos c Hc) in *. set (pos_d := Build_Z_pos d Hd) in *. set (pos_e := Build_Z_pos e He) in *. set (pos_f := Build_Z_pos f Hf) in *. set (pos_g := Build_Z_pos g Hg) in *. set (pos_h := Build_Z_pos h Hh) in *. generalize Habcd Hefgh Ha Hb Hc Hd He Hf Hg Hh. change ((0 < pos_a + pos_b + pos_c + pos_d)%Z -> (0 < pos_e + pos_f + pos_g + pos_h)%Z -> (0 <= pos_a)%Z -> (0 <= pos_b)%Z -> (0 <= pos_c)%Z -> (0 <= pos_d)%Z -> (0 <= pos_e)%Z -> (0 <= pos_f)%Z -> (0 <= pos_g)%Z -> (0 <= pos_h)%Z -> quadraticAcc pos_a pos_b pos_c pos_d pos_e pos_f pos_g pos_h p1 p2) in |- *. apply octet_lt_wf_rec_without_zeros_and_One with (P := fun (k l r s t u v w : Z) (p1 p2 : Qpositive) => (0 < k + l + r + s)%Z -> (0 < t + u + v + w)%Z -> (0 <= k)%Z -> (0 <= l)%Z -> (0 <= r)%Z -> (0 <= s)%Z -> (0 <= t)%Z -> (0 <= u)%Z -> (0 <= v)%Z -> (0 <= w)%Z -> quadraticAcc k l r s t u v w p1 p2). intros a0 b0 c0 d0 e0 f0 g0 h0 q1 q2 hyp1_aux. assert (hyp1 : forall (k l r s t u v w : Z) (p1 p2 : Qpositive), octet_lt k l r s t u v w p1 p2 a0 b0 c0 d0 e0 f0 g0 h0 q1 q2 -> (0 < k + l + r + s)%Z -> (0 < t + u + v + w)%Z -> (0 <= k)%Z -> (0 <= l)%Z -> (0 <= r)%Z -> (0 <= s)%Z -> (0 <= t)%Z -> (0 <= u)%Z -> (0 <= v)%Z -> (0 <= w)%Z -> quadraticAcc k l r s t u v w p1 p2). intros k l r s t u v w p3 p4. intros. change (quadraticAcc (Build_Z_pos k H2) (Build_Z_pos l H3) (Build_Z_pos r H4) (Build_Z_pos s H5) (Build_Z_pos t H6) (Build_Z_pos u H7) (Build_Z_pos v H8) (Build_Z_pos w H9) p3 p4) in |- *. apply hyp1_aux; repeat assumption. destruct q1 as [q| q| ]. destruct q2 as [q0| q0| ]. case (quadratic_top_more_informative a0 b0 c0 d0 e0 f0 g0 h0). intro t. intros. apply quadraticacc1; try discriminate. assumption. apply hyp1; [ right; split; [ reflexivity | apply quadratic_top_more_5; assumption ] | apply quadratic_top_more_1; assumption | assumption | idtac | idtac | idtac | idtac | assumption | assumption | assumption | assumption ]; apply Zle_minus; apply (quadratic_top_more_4_1 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_2 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_3 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_4 _ _ _ _ _ _ _ _ t). intro n. case (quadratic_top_more_informative e0 f0 g0 h0 a0 b0 c0 d0). intro t. intros. apply quadraticacc2; try discriminate; try assumption. apply hyp1; [ right; split; [ reflexivity | apply quadratic_top_more_5'; assumption ] | assumption | apply quadratic_top_more_1; assumption | assumption | assumption | assumption | assumption | idtac | idtac | idtac | idtac ]; apply Zle_minus; apply (quadratic_top_more_4_1 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_2 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_3 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_4 _ _ _ _ _ _ _ _ t). intro t. intros. apply quadraticacc3_II; try assumption. apply hyp1; [ left; unfold bin_lt in |- *; apply compare_nR | idtac | idtac | assumption | idtac | idtac | apply Zlt_le_weak; assumption | assumption | idtac | idtac | apply Zlt_le_weak; assumption ]; (replace 0%Z with (0 + 0)%Z; [ apply Zplus_le_lt_compat | constructor ]; [ repeat apply Zplus_le_0_compat | assumption ]; assumption) || (repeat apply Zplus_le_0_compat); assumption. case (quadratic_top_more_informative a0 b0 c0 d0 e0 f0 g0 h0). intro t. intros. apply quadraticacc1; try discriminate. assumption. apply hyp1; [ right; split; [ reflexivity | apply quadratic_top_more_5; assumption ] | apply quadratic_top_more_1; assumption | assumption | idtac | idtac | idtac | idtac | assumption | assumption | assumption | assumption ]; apply Zle_minus; apply (quadratic_top_more_4_1 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_2 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_3 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_4 _ _ _ _ _ _ _ _ t). intro n. case (quadratic_top_more_informative e0 f0 g0 h0 a0 b0 c0 d0). intro t. intros. apply quadraticacc2; try discriminate; try assumption. apply hyp1; [ right; split; [ reflexivity | apply quadratic_top_more_5'; assumption ] | assumption | apply quadratic_top_more_1; assumption | assumption | assumption | assumption | assumption | idtac | idtac | idtac | idtac ]; apply Zle_minus; apply (quadratic_top_more_4_1 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_2 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_3 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_4 _ _ _ _ _ _ _ _ t). intro t. intros. apply quadraticacc3_IO; try assumption. apply hyp1; [ left; unfold bin_lt in |- *; apply compare_nR | idtac | idtac | idtac | assumption | apply Zlt_le_weak; assumption | idtac | idtac | assumption | apply Zlt_le_weak; assumption | idtac ]; (replace 0%Z with (0 + 0 + 0)%Z; [ apply Zplus_lt_le_compat; [ apply Zplus_le_lt_compat; try assumption | idtac ] | constructor ]; repeat apply Zplus_le_0_compat; assumption) || (repeat apply Zplus_le_0_compat); assumption. intros. apply quadraticacc0'. discriminate. constructor. apply homographicAcc_wf; (rewrite Zplus_assoc; assumption) || (repeat apply Zplus_le_0_compat; try assumption). destruct q2 as [q0| q0| ]. case (quadratic_top_more_informative a0 b0 c0 d0 e0 f0 g0 h0). intro t. intros. apply quadraticacc1; try discriminate. assumption. apply hyp1; [ right; split; [ reflexivity | apply quadratic_top_more_5; assumption ] | apply quadratic_top_more_1; assumption | assumption | idtac | idtac | idtac | idtac | assumption | assumption | assumption | assumption ]; apply Zle_minus; apply (quadratic_top_more_4_1 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_2 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_3 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_4 _ _ _ _ _ _ _ _ t). intro n. case (quadratic_top_more_informative e0 f0 g0 h0 a0 b0 c0 d0). intro t. intros. apply quadraticacc2; try discriminate; try assumption. apply hyp1; [ right; split; [ reflexivity | apply quadratic_top_more_5'; assumption ] | assumption | apply quadratic_top_more_1; assumption | assumption | assumption | assumption | assumption | idtac | idtac | idtac | idtac ]; apply Zle_minus; apply (quadratic_top_more_4_1 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_2 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_3 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_4 _ _ _ _ _ _ _ _ t). intro t. intros. apply quadraticacc3_OI; try assumption. apply hyp1; [ left; unfold bin_lt in |- *; apply compare_dL | idtac | idtac | idtac | apply Zlt_le_weak; assumption | assumption | idtac | idtac | apply Zlt_le_weak; assumption | assumption | idtac ]; (replace 0%Z with (0 + 0 + 0 + 0)%Z; [ apply Zplus_lt_le_compat; [ apply Zplus_lt_le_compat; [ apply Zplus_le_lt_compat | idtac ] | idtac ] | constructor ]; try apply Zplus_le_0_compat; assumption) || (repeat apply Zplus_le_0_compat); assumption. case (quadratic_top_more_informative a0 b0 c0 d0 e0 f0 g0 h0). intro t. intros. apply quadraticacc1; try discriminate. assumption. apply hyp1; [ right; split; [ reflexivity | apply quadratic_top_more_5; assumption ] | apply quadratic_top_more_1; assumption | assumption | idtac | idtac | idtac | idtac | assumption | assumption | assumption | assumption ]; apply Zle_minus; apply (quadratic_top_more_4_1 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_2 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_3 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_4 _ _ _ _ _ _ _ _ t). intro n. case (quadratic_top_more_informative e0 f0 g0 h0 a0 b0 c0 d0). intro t. intros. apply quadraticacc2; try discriminate; try assumption. apply hyp1; [ right; split; [ reflexivity | apply quadratic_top_more_5'; assumption ] | assumption | apply quadratic_top_more_1; assumption | assumption | assumption | assumption | assumption | idtac | idtac | idtac | idtac ]; apply Zle_minus; apply (quadratic_top_more_4_1 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_2 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_3 _ _ _ _ _ _ _ _ t) || apply (quadratic_top_more_4_4 _ _ _ _ _ _ _ _ t). intro t. intros. apply quadraticacc3_OO; try assumption. apply hyp1; [ left; unfold bin_lt in |- *; apply compare_dL | idtac | idtac | apply Zlt_le_weak; assumption | idtac | idtac | assumption | apply Zlt_le_weak; assumption | idtac | idtac | assumption ]; (replace 0%Z with (0 + 0 + 0 + 0)%Z; [ repeat apply Zplus_lt_le_compat | constructor ]; try apply Zplus_le_0_compat; assumption) || (repeat apply Zplus_le_0_compat); assumption. intros. apply quadraticacc0'. discriminate. constructor. apply homographicAcc_wf; (rewrite Zplus_assoc; assumption) || (repeat apply Zplus_le_0_compat; try assumption). intros. apply quadraticacc0. reflexivity. apply homographicAcc_wf; (apply Zplus_le_0_compat; assumption) || (rewrite Zplus_assoc; (rewrite Zplus_assoc_reverse with (m := c0:Z); rewrite Z.add_comm with (n := c0:Z)) || (rewrite Zplus_assoc_reverse with (m := g0:Z); rewrite Z.add_comm with (n := g0:Z)); rewrite Zplus_assoc); assumption. Qed.
imports: QArithSternBrocot(Merge_Order)