proposition: Lemma sep__part_fun_mon_pts : forall (i : nat) Hi Hi' Hi0 Hi'0, P (sep__part_fun i Hi) Hi0[<]P (sep__part_fun (S i) Hi') Hi'0.
proof: Proof. do 3 intro. rewrite sep__part_fun_i. 2: auto with arith. elim (le_lt_eq_dec _ _ Hi'); intro. rewrite (sep__part_fun_i (S i)). 2: assumption. intros. apply sep__part_h_lemma. rewrite <- sep__part_fun_i with (H := Hi'). apply sep__part_fun_bnd'; assumption. assumption. generalize Hi'; clear Hi'; rewrite b0. intro; rewrite sep__part_fun_m. intros. cut (m = m). 2: auto. unfold m at 2 in |- *; elim (RS'_delta2_delta4 RS'_m1); intro; simpl in |- *; intro. cut (i = RS'_m1); [ clear b0; intro | rewrite <- b0 in H; auto with arith ]. generalize Hi0; clear Hi0; rewrite H0. intro. elim (ProjT2 sep__part_app_n); fold RS'_m1 in |- *; intros. apply less_transitive_unfolded with (P (sep__part_h RS'_m1) Hi0[+]delta [/]FourNZ). apply shift_less_plus'; astepl ZeroR; apply pos_div_four; apply RS'_delta_pos. apply shift_plus_less'; eapply less_wdr. apply a0. apply cg_minus_wd; apply prf1. auto. auto. elim (ProjT2 sep__part_app_n); fold RS'_m1 in |- *; intros. generalize Hi'0; clear Hi'0. cut (S i = RS'_m1); [ intro | transitivity m; auto ]. pattern n at 1 5 in |- *; rewrite <- H0. rewrite <- H2. intro. apply less_leEq_trans with (P _ (sep__part_h_bnd (S i))). 2: apply local_mon'_imp_mon'_le with (f := fun (i : nat) (Hi : i <= n) => P i Hi). 2: intros; apply prf2. 2: red in |- *; intros; apply prf1; assumption. 2: apply sep__part_h_mon_1. apply sep__part_h_lemma. apply H1. rewrite H2; apply le_n. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)