proposition: Lemma sep__part_app_n : {m : nat | sep__part_h (S m) = n /\ (forall i : nat, i <= m -> sep__part_h i < n)}.
proof: Proof. elim (weird_mon_covers _ _ sep__part_h_mon_2); intros m Hm Hm'. set (m' := pred m) in *. exists m'. cut (m <> 0); intro. split. cut (S m' = m); [ intro | unfold m' in |- *; apply Nat.lt_succ_pred with 0; apply Nat.neq_0_lt_0; auto ]. rewrite H0; clear H0 m'. cut (n <= sep__part_h m). cut (sep__part_h m <= n); intros. auto with arith. apply sep__part_h_bnd. assumption. intros; apply Hm'. unfold m' in H0; rewrite <- (Nat.lt_succ_pred 0 m); auto with arith. apply Nat.neq_0_lt_0; auto. apply SPap_n. rewrite H in Hm. simpl in Hm. apply Nat.le_antisymm; auto with arith. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)