proposition: Lemma sep__part_Sum4 : Sumx (fun (i : nat) (Hi : i < m) => Sum2 (fun (j : nat) (Hj : sep__part_fun i (Nat.lt_le_incl _ _ Hi) <= j) (Hj' : j <= pred (sep__part_fun (S i) Hi)) => (M[+]M)[*]delta [/]TwoNZ))[<=]alpha.
proof: Proof. unfold Sum2 in |- *. apply leEq_wdl with (Sumx (fun (j : nat) (_ : j < n) => part_tot_nat_fun _ _ (fun (i : nat) (_ : i < n) => (M[+]M)[*]delta [/]TwoNZ) j)). 2: apply eq_symmetric_unfolded; apply str_Sumx_Sum_Sum' with (g := fun (i : nat) (Hi : i < m) (i0 : nat) => sumbool_rect (fun _ : {sep__part_fun i (Nat.lt_le_incl i m Hi) <= i0} + {i0 < sep__part_fun i (Nat.lt_le_incl i m Hi)} => IR) (fun _ : sep__part_fun i (Nat.lt_le_incl i m Hi) <= i0 => sumbool_rect (fun _ : {i0 <= pred (sep__part_fun (S i) Hi)} + {pred (sep__part_fun (S i) Hi) < i0} => IR) (fun _ : i0 <= pred (sep__part_fun (S i) Hi) => (M[+]M)[*]delta [/]TwoNZ) (fun _ : pred (sep__part_fun (S i) Hi) < i0 => [0]) (le_lt_dec i0 (pred (sep__part_fun (S i) Hi)))) (fun _ : i0 < sep__part_fun i (Nat.lt_le_incl i m Hi) => [0]) (le_lt_dec (sep__part_fun i (Nat.lt_le_incl i m Hi)) i0)) (h := part_tot_nat_fun _ _ (fun (i : nat) (_ : i < n) => (M[+]M)[*]delta [/]TwoNZ)). apply leEq_wdr with (Sumx (fun (i : nat) (_ : i < n) => alpha[/] _[//]nring_ap_zero _ _ SPap_n)). 2: rstepr (nring n[*](alpha[/] _[//]nring_ap_zero _ _ SPap_n)); apply sumx_const. apply Sumx_resp_leEq; intros. unfold part_tot_nat_fun in |- *. elim (le_lt_dec n i); intro; simpl in |- *. exfalso; lia. unfold delta in |- *. apply leEq_transitive with ((M[+]M)[*] (alpha[/] _[//] mult_resp_ap_zero _ _ _ (nring_ap_zero _ _ SPap_n) (max_one_ap_zero M)) [/]TwoNZ). apply mult_resp_leEq_lft. apply div_resp_leEq. apply pos_two. apply Min_leEq_rht. astepl (ZeroR[+][0]); apply plus_resp_leEq_both; unfold M in |- *; apply positive_norm. rstepl (alpha[*](M[/] _[//]max_one_ap_zero M)[*] ([1][/] _[//]nring_ap_zero _ _ SPap_n)). rstepr (alpha[*][1][*]([1][/] _[//]nring_ap_zero _ _ SPap_n)). apply mult_resp_leEq_rht. apply mult_resp_leEq_lft. apply shift_div_leEq. apply pos_max_one. astepr (Max M [1]); apply lft_leEq_Max. apply less_leEq; assumption. apply less_leEq; apply recip_resp_pos. astepl (nring (R:=IR) 0); apply nring_less; apply RS'_pos_n. apply sep__part_fun_0. exact sep__part_fun_wd. exact sep__part_fun_mon. unfold part_tot_nat_fun in |- *. intros; elim (le_lt_dec (sep__part_fun i (Nat.lt_le_incl _ _ Hi)) j); intro; simpl in |- *. elim (le_lt_dec j (pred (sep__part_fun (S i) Hi))); intro; simpl in |- *. elim (le_lt_dec n j); intro; simpl in |- *. exfalso; apply (Nat.le_ngt n j). assumption. eapply Nat.lt_le_trans. apply H0. apply sep__part_fun_bnd. algebra. exfalso; apply (proj1 (Nat.le_ngt _ _) H0). rewrite <- (Nat.lt_succ_pred (sep__part_fun i Hi') (sep__part_fun (S i) Hi'')). cut (sep__part_fun (S i) Hi'' = sep__part_fun (S i) Hi); [ intro | apply sep__part_fun_wd; auto ]. rewrite H1; auto with arith. apply sep__part_fun_mon. apply Nat.lt_succ_diag_r. exfalso; apply (proj1 (Nat.le_ngt _ _) H). rewrite sep__part_fun_i. 2: assumption. rewrite sep__part_fun_i in b0; assumption. intros; symmetry in |- *; apply sep__part_fun_m. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)