proposition: Lemma compact_bnd_AbsIR : forall x y d H, compact (x[-]d) (x[+]d) H y -> AbsIR (x[-]y) [<=] d.
proof: Proof. intros x y d H H0. inversion_clear H0. simpl in |- *; unfold ABSIR in |- *. apply Max_leEq. apply shift_minus_leEq; apply shift_leEq_plus'; auto. rstepl (y[-]x). apply shift_minus_leEq. astepr (x[+]d); auto. Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists