proposition: Lemma sep__sep_fun_i_delta : forall (i : nat) (Hi Hi' : i <= n) (Hi0 : i < n), AbsIR (sep__sep_fun_i i Hi[-]P i Hi')[<=]delta [/]TwoNZ.
proof: Proof. intros. unfold sep__sep_fun_i in |- *. elim (sep__sep_aux_lemma i); intro; simpl in |- *. apply eq_imp_leEq. eapply eq_transitive_unfolded. 2: apply AbsIR_eq_x. apply AbsIR_wd. rstepr (P i Hi'[+]delta [/]TwoNZ[-]P i Hi'). apply cg_minus_wd. apply bin_op_wd_unfolded. apply prf1; auto. algebra. algebra. astepr (delta [/]TwoNZ); apply less_leEq; apply pos_div_two; exact RS_delta_pos. apply leEq_wdl with ZeroR. astepr (delta [/]TwoNZ); apply less_leEq; apply pos_div_two; exact RS_delta_pos. eapply eq_transitive_unfolded. apply eq_symmetric_unfolded; apply AbsIRz_isz. apply AbsIR_wd. astepl (P i Hi[-]P i Hi). apply cg_minus_wd; apply prf1; auto. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions