proposition: Lemma sep__part_h_mon_3 : forall i j : nat, sep__part_h i < n -> i < j -> sep__part_h i < sep__part_h j.
proof: Proof. intros; induction j as [| j Hrecj]. exfalso; inversion H0. cut (sep__part_h j <= sep__part_h (S j)); intros. 2: apply sep__part_h_mon_1. elim (le_lt_eq_dec _ _ H0); intro. apply Nat.lt_le_trans with (sep__part_h j); auto. apply Hrecj; auto with arith. rewrite <- b0; apply sep__part_h_mon_2; auto. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)