proposition: Lemma sep__part_mon : forall (i : nat) Hi Hi', sep__part i Hi[<]sep__part (S i) Hi'.
proof: Proof. intros. unfold sep__part in |- *; simpl in |- *. apply sep__part_fun_mon_pts. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)