proposition: Lemma sep__part_h_mon_2 : forall i : nat, sep__part_h i < n -> sep__part_h i < sep__part_h (S i).
proof: Proof. intros; 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 *; fold j in |- *. elim (ProjT2 a1); intros Hj Hj'; fold j in Hj, Hj'. elim Hj'; clear Hj'; intros Hj0 Hj1. apply (Partition_Points_mon _ _ _ _ P) with a0 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. assumption. assumption. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)