proposition: Lemma sep__part_aux : forall i : nat, pred (sep__part_h (S i)) < n.
proof: Proof. intros. red in |- *. rewrite Nat.lt_succ_pred with (sep__part_h 0) (sep__part_h (S i)). apply sep__part_h_bnd. apply sep__part_h_mon_3. rewrite <- sep__part_fun_i with (H := Nat.le_0_l m). 2: apply RS'_pos_m. 2: apply Nat.lt_0_succ. rewrite <- sep__part_fun_m with (H := le_n m). apply sep__part_fun_mon. apply RS'_pos_m. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)