proposition: Lemma sep__sep_aux : forall (i : nat) (H : i < n) Hg Hs, AbsIR (F (g i H) Hg[-]F (sep__sep_points i H) Hs)[<=]e.
proof: Proof. intros. apply RS_Hd'. unfold I in |- *; apply Pts_part_lemma with n P; assumption. unfold I in |- *; apply Pts_part_lemma with n sep__sep_part; apply sep__sep_points_lemma. unfold sep__sep_points in |- *; simpl in |- *. eapply leEq_wdl. 2: apply AbsIR_minus. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. apply shift_minus_leEq; apply Max_leEq. unfold sep__sep_fun_i in |- *. elim sep__sep_aux_lemma; intro; simpl in |- *. apply leEq_transitive with (P i (Nat.lt_le_incl _ _ H)[+]delta). apply plus_resp_leEq_lft. apply less_leEq; astepl (delta [/]TwoNZ); apply pos_div_two'; exact RS_delta_pos. eapply leEq_wdr. 2: apply cag_commutes_unfolded. apply plus_resp_leEq_both. elim (gP i H); intros; assumption. apply RS_delta_d. astepl ([0][+]P i (Nat.lt_le_incl _ _ H)). apply plus_resp_leEq_both. apply less_leEq; exact RS_Hd. elim (gP i H); intros; auto. apply shift_leEq_plus; astepl ZeroR; apply less_leEq; exact RS_Hd. apply shift_leEq_minus. eapply leEq_wdl. apply rht_leEq_Max. algebra. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions