proposition: Lemma sep__part_h_bnd : forall i : nat, sep__part_h i <= n.
proof: Proof. intro. induction i as [| i Hreci]. apply Nat.le_0_l. 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'. assumption. apply le_n. apply le_n. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)