proposition: Lemma sep__part_fun_m : forall H : m <= m, sep__part_fun m H = n.
proof: Proof. intros. unfold sep__part_fun in |- *. elim (le_lt_eq_dec _ _ H); intro; simpl in |- *. elim (Nat.lt_irrefl _ a0). reflexivity. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)