proposition: Lemma sep__part_fun_i' : forall (i : nat) (H : i <= m), sep__part_h i <= sep__part_fun i H.
proof: Proof. intros. unfold sep__part_fun in |- *. elim (le_lt_eq_dec _ _ H); intro; simpl in |- *. apply le_n. apply sep__part_h_bnd. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)