proposition: Lemma sep__sep_fun_delta : forall (i : nat) (Hi Hi' : i <= n), AbsIR (sep__sep_fun i Hi[-]P i Hi')[<=]delta [/]TwoNZ.
proof: Proof. intros. unfold sep__sep_fun in |- *. elim (le_lt_dec i 0); intro; simpl in |- *. cut (i = 0); [ intro | auto with arith ]. generalize Hi'; rewrite H; intros. 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 (a[-]a). apply cg_minus_wd; [ algebra | apply eq_symmetric_unfolded; apply start ]. elim (le_lt_eq_dec _ _ Hi); intro; simpl in |- *. apply sep__sep_fun_i_delta; assumption. generalize Hi'; rewrite b1; intros. 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 (b[-]b). apply cg_minus_wd; [ algebra | apply eq_symmetric_unfolded; apply finish ]. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions