proposition: Lemma sep__sep_less : forall Hi' : S i <= n, sep__sep_fun_i[<]P (S i) Hi'.
proof: Proof. unfold sep__sep_fun_i in |- *. elim sep__sep_aux_lemma; intros; simpl in |- *. 2: apply HP. apply shift_plus_less'. apply less_leEq_trans with delta. astepl (delta [/]TwoNZ). apply pos_div_two'; exact RS_delta_pos. apply leEq_transitive with deltaP. apply RS_delta_deltaP. unfold deltaP in |- *; apply AntiMesh_lemma. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions