proposition: Lemma sep__sep_leEq : forall Hi' : i <= n, P i Hi'[<=]sep__sep_fun_i.
proof: Proof. unfold sep__sep_fun_i in |- *. elim sep__sep_aux_lemma; intros; simpl in |- *. 2: apply eq_imp_leEq; apply prf1; auto. apply leEq_wdl with (P i Hi). 2: apply prf1; auto. apply shift_leEq_plus'; astepl ZeroR. astepr (delta [/]TwoNZ). apply less_leEq; apply pos_div_two; exact RS_delta_pos. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions