proposition: Lemma compact_elements' : forall c d Hcd x y, Compact Hab x -> compact c d Hcd y -> AbsIR (x[-]y) [<=] AbsIR (Max b d[-]Min a c).
proof: Proof. do 5 intro; intros Hx Hy. eapply leEq_transitive. 2: apply leEq_AbsIR. inversion_clear Hx. inversion_clear Hy. simpl in |- *; unfold ABSIR in |- *; apply Max_leEq. unfold cg_minus in |- *; apply plus_resp_leEq_both. apply leEq_transitive with b; auto; apply lft_leEq_Max. apply inv_resp_leEq; apply leEq_transitive with c; auto; apply Min_leEq_rht. rstepl (y[-]x). unfold cg_minus in |- *; apply plus_resp_leEq_both. apply leEq_transitive with d; auto; apply rht_leEq_Max. apply inv_resp_leEq; apply leEq_transitive with a; auto; apply Min_leEq_lft. Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists