proposition: Lemma sep__sep_mon_i : forall (i : nat) (Hi : i <= n) (Hi' : S i <= n) (Hi0 : i < n), sep__sep_fun_i i Hi[<]sep__sep_fun_i (S i) Hi'.
proof: Proof. intros. apply less_leEq_trans with (P (S i) Hi0). apply sep__sep_less. apply sep__sep_leEq. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions