proposition: Lemma compact_wd' : forall (a' b' : IR) Hab' (x : IR), a [=] a' -> b [=] b' -> compact a b Hab x -> compact a' b' Hab' x.
proof: Proof. intros a' b' Hab' x H H0 H1. inversion_clear H1; split. apply leEq_wdl with a; auto. apply leEq_wdr with b; auto. Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists