proposition: Lemma sep__sep_ap : forall (j : nat) (Hj : j <= m), sep__sep_fun_i[#]R j Hj.
proof: Proof. intros. unfold sep__sep_fun_i in |- *; elim sep__sep_aux_lemma; intro; simpl in |- *. 2: apply zero_minus_apart; apply AbsIR_cancel_ap_zero; apply Greater_imp_ap. elim a0; intros j' H. elim H; clear a0 H; intros Hj' H. unfold pred1 in H. rstepr (P i Hi[+](R j Hj[-]P i Hi)). apply op_lft_resp_ap. apply un_op_strext_unfolded with AbsIR. apply ap_wdl_unfolded with (delta [/]TwoNZ). 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply less_leEq; apply pos_div_two; exact RS_delta_pos. eapply ap_wdr_unfolded. 2: apply AbsIR_minus. elim (le_lt_dec j j'); intro. elim (le_lt_eq_dec _ _ a0); clear a0; intro. apply less_imp_ap; apply separation_conseq with j' Hj'. apply H. intro; rewrite H0 in a0; apply (Nat.lt_irrefl _ a0). apply Greater_imp_ap. eapply less_wdl. apply H with (Hi' := Hi). apply AbsIR_wd. apply cg_minus_wd. algebra. apply prf1; auto. apply less_imp_ap; apply separation_conseq with j' Hj'. apply H. intro; rewrite H0 in b0; apply (Nat.lt_irrefl _ b0). unfold pred2 in b0. eapply less_transitive_unfolded. 2: apply b0. apply pos_div_four; exact RS_delta_pos. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions