proposition: Lemma sep__part_fun_mon : forall (i j : nat) Hi Hj, i < j -> sep__part_fun i Hi < sep__part_fun j Hj.
proof: Proof. intros. apply less_nring with (IR:COrdField). apply local_mon_imp_mon_le with (f := fun (i : nat) (Hi : i <= m) => nring (R:=IR) (sep__part_fun i Hi)). clear H Hj Hi j i; intros; apply nring_less. 2: assumption. elim (le_lt_eq_dec _ _ H'); intro. rewrite (sep__part_fun_i (S i)). 2: assumption. simpl in |- *; elim (le_lt_dec (sep__part_h i) n); intro; simpl in |- *. elim (sep__part_lemma (sep__part_h i) a1); intro; simpl in |- *. elim (ProjT2 a2); set (j := ProjT1 a2) in *. intros Hj Hj'. elim Hj'; clear Hj'; intros H0 H1. rewrite sep__part_fun_i. 2: auto with arith. apply (Partition_Points_mon _ _ _ _ P) with a1 Hj. apply less_transitive_unfolded with (P _ a1[+]delta [/]FourNZ). apply shift_less_plus'; astepl ZeroR; apply pos_div_four; exact RS'_delta_pos. apply shift_plus_less'; apply H0. apply sep__part_fun_bnd'; auto with arith. apply sep__part_fun_bnd'; auto with arith. generalize H'; rewrite b0. intro; rewrite sep__part_fun_m. apply sep__part_fun_bnd'. auto with arith. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)