proposition: Lemma compact_elements : forall x y : IR, Compact Hab x -> Compact Hab y -> AbsIR (x[-]y) [<=] AbsIR (b[-]a).
proof: Proof. clear Hab' He e. do 2 intro; intros Hx Hy. apply leEq_wdr with (b[-]a). 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply shift_leEq_minus; astepl a; auto. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply Abs_Max. inversion_clear Hx. inversion_clear Hy. unfold cg_minus in |- *; apply plus_resp_leEq_both. apply Max_leEq; auto. apply inv_resp_leEq. apply leEq_Min; auto. Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists