proposition: Lemma sep__sep_Mesh : Mesh sep__sep_part[<=]Mesh P[+]csi.
proof: Proof. unfold Mesh in |- *. apply maxlist_leEq. apply length_Part_Mesh_List. exact RS_pos_n. intros x H. elim (Part_Mesh_List_lemma _ _ _ _ _ _ H); intros i Hi. elim Hi; clear Hi; intros Hi Hi'. elim Hi'; clear Hi'; intros Hi' Hx. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply Hx. unfold sep__sep_part in |- *; simpl in |- *. unfold sep__sep_fun in |- *; simpl in |- *. elim (le_lt_dec (S i) 0); intro; simpl in |- *. exfalso; inversion a0. elim (le_lt_eq_dec _ _ Hi'); intro; simpl in |- *. elim (le_lt_dec i 0); intro; simpl in |- *. cut (i = 0); [ intro | auto with arith ]. unfold sep__sep_fun_i in |- *; simpl in |- *. elim (sep__sep_aux_lemma (S i)); intro; simpl in |- *. generalize Hi'; rewrite H0; clear Hx Hi'; intro. apply leEq_wdl with (P 1 Hi'[+]delta [/]TwoNZ[-]P 0 (Nat.le_0_l _)). rstepl (P 1 Hi'[-]P 0 (Nat.le_0_l _)[+]delta [/]TwoNZ). apply plus_resp_leEq_both. fold (Mesh P) in |- *; apply Mesh_lemma. apply leEq_transitive with delta. apply less_leEq; apply pos_div_two'; exact RS_delta_pos. apply RS_delta_csi. apply cg_minus_wd; [ algebra | apply start ]. generalize Hi'; rewrite H0; clear Hx Hi'; intro. apply leEq_wdl with (P 1 Hi'[-]P 0 (Nat.le_0_l _)). fold (Mesh P) in |- *; apply leEq_transitive with (Mesh P[+][0]). astepr (Mesh P); apply Mesh_lemma. apply plus_resp_leEq_lft. apply less_leEq; assumption. apply cg_minus_wd; [ algebra | apply start ]. elim (le_lt_eq_dec _ _ Hi); intro; simpl in |- *. unfold sep__sep_fun_i in |- *. elim (sep__sep_aux_lemma (S i)); elim (sep__sep_aux_lemma i); intros; simpl in |- *. rstepl (P (S i) Hi'[-]P i Hi). fold (Mesh P) in |- *; apply leEq_transitive with (Mesh P[+][0]). astepr (Mesh P); apply Mesh_lemma. apply plus_resp_leEq_lft. apply less_leEq; assumption. rstepl (P _ Hi'[-]P _ Hi[+]delta [/]TwoNZ). apply plus_resp_leEq_both. fold (Mesh P) in |- *; apply Mesh_lemma. apply leEq_transitive with delta. apply less_leEq; apply pos_div_two'; exact RS_delta_pos. apply RS_delta_csi. rstepl (P _ Hi'[-]P _ Hi[-]delta [/]TwoNZ). unfold cg_minus at 1 in |- *; apply plus_resp_leEq_both. fold (Mesh P) in |- *; apply Mesh_lemma. apply leEq_transitive with ZeroR. astepr ([--]ZeroR); apply inv_resp_leEq. apply less_leEq; apply pos_div_two; exact RS_delta_pos. apply leEq_transitive with delta. apply less_leEq; exact RS_delta_pos. apply RS_delta_csi. fold (Mesh P) in |- *; apply leEq_transitive with (Mesh P[+][0]). astepr (Mesh P); apply Mesh_lemma. apply plus_resp_leEq_lft. apply less_leEq; assumption. exfalso; rewrite b2 in a0; apply Nat.lt_irrefl with (S n); apply Nat.lt_trans with (S n); auto with arith. elim (le_lt_dec i 0); intro; simpl in |- *. cut (i = 0); [ intro | auto with arith ]. rewrite H0 in b1. clear Hx; rewrite H0 in Hi'. apply leEq_wdl with (P 1 Hi'[-]P 0 (Nat.le_0_l n)). fold (Mesh P) in |- *; apply leEq_transitive with (Mesh P[+][0]). astepr (Mesh P); apply Mesh_lemma. apply plus_resp_leEq_lft. apply less_leEq; assumption. apply cg_minus_wd. generalize Hi'; rewrite b1; intro; apply finish. apply start. elim (le_lt_eq_dec _ _ Hi); intro; simpl in |- *. unfold sep__sep_fun_i in |- *. elim (sep__sep_aux_lemma i); intro; simpl in |- *. apply leEq_wdl with (P (S i) Hi'[-](P i Hi[+]delta [/]TwoNZ)). rstepl (P (S i) Hi'[-]P i Hi[-]delta [/]TwoNZ). unfold cg_minus at 1 in |- *; apply plus_resp_leEq_both. fold (Mesh P) in |- *; apply Mesh_lemma. apply leEq_transitive with ZeroR. astepr ([--]ZeroR); apply inv_resp_leEq. apply less_leEq; apply pos_div_two; exact RS_delta_pos. apply leEq_transitive with delta. apply less_leEq; exact RS_delta_pos. apply RS_delta_csi. apply cg_minus_wd. generalize Hi'; rewrite b1; intro; apply finish. algebra. apply leEq_wdl with (P (S i) Hi'[-]P i Hi). fold (Mesh P) in |- *; apply leEq_transitive with (Mesh P[+][0]). astepr (Mesh P); apply Mesh_lemma. apply plus_resp_leEq_lft. apply less_leEq; assumption. apply cg_minus_wd. generalize Hi'; rewrite b1; intro; apply finish. algebra. exfalso; rewrite b3 in b1; apply n_Sn with n; auto. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions