proposition: Lemma sep__part_mon_Mesh : Mesh sep__part[<=]Mesh P[+]csi.
proof: Proof. unfold Mesh at 1 in |- *. apply maxlist_leEq. apply length_Part_Mesh_List. apply RS'_pos_m. 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. clear Hx H x. simpl in |- *. cut (forall Ha Hb, P (sep__part_fun (S i) Hi') Ha[-]P (sep__part_fun i Hi) Hb[<=]Mesh P[+]csi). intro. apply H. rename Hi' into H. rewrite (sep__part_fun_i i). 2: assumption. elim (le_lt_eq_dec _ _ H); intro. rewrite sep__part_fun_i. 2: assumption. intros. cut (pred (sep__part_h (S i)) <= n); [ intro | eapply Nat.le_trans; [ apply Nat.le_pred_l | auto ] ]. rstepl (P _ Ha[-]P _ H0[+](P _ H0[-]P _ Hb)). apply plus_resp_leEq_both. generalize Ha; pattern (sep__part_h (S i)) at 1 2 in |- *; replace (sep__part_h (S i)) with (S (pred (sep__part_h (S i)))); intros. apply Mesh_lemma. apply Nat.lt_succ_pred with (sep__part_h i); apply sep__part_h_mon_2. rewrite <- sep__part_fun_i with (H := Nat.lt_le_incl _ _ H). apply sep__part_fun_bnd'; assumption. assumption. eapply leEq_transitive. apply sep__part_h_lemma2. apply less_leEq; apply less_leEq_trans with delta. apply pos_div_two'; exact RS'_delta_pos. apply RS'_delta_csi. generalize H; clear H; rewrite b0; intro H. rewrite sep__part_fun_m. cut (m = m); [ unfold m at 2 in |- * | auto ]. elim RS'_delta2_delta4; intro; simpl in |- *; intro. intros. cut (sep__part_h (S RS'_m1) = n). intro; generalize Ha Hb; pattern n at 1 5 in |- *. rewrite <- H1. cut (i = RS'_m1); [ intro | unfold sep__part_length in b0; rewrite <- b0 in H0; auto with arith ]. rewrite H2. intros. cut (pred (sep__part_h (S RS'_m1)) <= n); [ intro | eapply Nat.le_trans; [ apply Nat.le_pred_l | auto ] ]. rstepl (P _ Ha0[-]P _ H3[+](P _ H3[-]P _ Hb0)). apply plus_resp_leEq_both. generalize Ha0; pattern (sep__part_h (S RS'_m1)) at 1 2 in |- *; replace (sep__part_h (S RS'_m1)) with (S (pred (sep__part_h (S RS'_m1)))); intros. apply Mesh_lemma. apply Nat.lt_succ_pred with (sep__part_h RS'_m1); apply sep__part_h_mon_2. cut (RS'_m1 <= m). 2: rewrite H0; apply Nat.le_succ_diag_r. intro. rewrite <- sep__part_fun_i with (H := H4). apply sep__part_fun_bnd'. rewrite H0; apply Nat.lt_succ_diag_r. rewrite H0; apply Nat.lt_succ_diag_r. eapply leEq_transitive. apply sep__part_h_lemma2. apply less_leEq; apply less_leEq_trans with delta. apply pos_div_two'; exact RS'_delta_pos. apply RS'_delta_csi. elim (ProjT2 sep__part_app_n); fold RS'_m1 in |- *; intros. auto. cut (sep__part_h (S RS'_m1) = n). intro; pattern n at 1 5 in |- *. rewrite <- H1. intros. cut (sep__part_h RS'_m1 <= n); [ intro | apply sep__part_h_bnd ]. rstepl (P _ Ha[-]P _ H2[+](P _ H2[-]P _ Hb)). apply leEq_transitive with (delta [/]TwoNZ[+](Mesh P[+]delta [/]TwoNZ)). apply plus_resp_leEq_both. apply less_leEq; eapply less_wdl. apply b1. apply cg_minus_wd; apply prf1; auto. generalize H2; clear H2; rewrite <- H0; unfold sep__part_length in b0; rewrite <- b0. simpl in |- *. elim (le_lt_dec (sep__part_h i) n); intro; simpl in |- *. elim (sep__part_lemma (sep__part_h i) a0); intro; simpl in |- *. set (j := ProjT1 a1) in *. change (forall H0, P j H0[-]P (sep__part_h i) Hb[<=]Mesh P[+]delta [/]TwoNZ) in |- *. elim (ProjT2 a1); fold j in |- *; intros Hj Hj'. elim Hj'; clear Hj'; intros H2 H3. intros. cut (pred j <= n); [ intro | apply Nat.le_trans with j; auto with arith ]. rstepl (P j H4[-]P (pred j) H5[+](P (pred j) H5[-]P (sep__part_h i) Hb)). cut (0 < j); intros. apply plus_resp_leEq_both. cut (j = S (pred j)); [ intro | symmetry; apply Nat.lt_succ_pred with 0; auto ]. generalize H4 H5 H6; rewrite H7; intros. apply Mesh_lemma. apply less_leEq. apply less_wdl with (P (pred j) H5[-]P _ a0). 2: apply cg_minus_wd; apply prf1; auto. apply H3. auto with arith. apply Nat.le_lt_trans with (sep__part_h i); auto with arith. apply Partition_Points_mon with (P := P) (Hi := a0) (Hj := Hj). apply less_transitive_unfolded with (P (sep__part_h i) a0[+]delta [/]FourNZ). apply shift_less_plus'; astepl ZeroR; apply pos_div_four; exact RS'_delta_pos. apply shift_plus_less'; assumption. intros. apply less_leEq; apply less_leEq_trans with (delta [/]TwoNZ). eapply less_wdl. apply b2. apply cg_minus_wd; apply prf1; auto. astepl ([0][+]delta [/]TwoNZ); apply plus_resp_leEq; apply Mesh_nonneg. exfalso. lia. rstepl (Mesh P[+]delta). apply plus_resp_leEq_lft; apply RS'_delta_csi. elim (ProjT2 sep__part_app_n); fold RS'_m1 in |- *; intros. auto. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)