proposition: Lemma CompactImage_b_correct1 : forall (x : Complete X) (s : Compact X), inCompact x s -> inCompact (Cbind plX f x) (CompactImage_b s).
proof: Proof. intros x s H. change (inCompact (Cjoin (Cmap_fun plX f x)) (CompactCompleteCompact _ (CompactImage z plFEX f s))). rewrite <- CompactCompleteCompact_correct. apply CompactImage_correct1;assumption. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Limit CoRN.metric2.FinEnum Coq.ZArith.Zpow_facts CoRN.metric2.Complete CoRN.logic.Classic Coq.QArith.Qpower Coq.QArith.Qround CoRN.metric2.Prelength