proposition: Lemma compact_wd : pred_wd IR (compact a b Hab).
proof: Proof. intros; red in |- *; intros x y H H0. inversion_clear H; split. apply leEq_wdr with x; assumption. apply leEq_wdl with x; assumption. Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists