proposition: Lemma graphQ_bonus : forall e x y, In (x, y) (approximate (graphQ (uc_compose clip f)) e) -> l <= x <= r /\ b <= y <= t.
proof: Proof. intros [e|] x y;[|intros; contradiction]. simpl. unfold Cjoin_raw. Opaque CompactIntervalQ. simpl. unfold FinCompact_raw. rewrite map_map. rewrite -> in_map_iff. unfold graphPoint_b_raw; simpl. unfold Couple_raw; simpl. intros [z [Hz0 Hz1]]. inversion Hz0. subst x. subst y. clear Hz0. split. eapply CompactIntervalQ_bonus_correct. apply Hz1. split. apply Qmax_ub_l. apply Qmax_lub. rewrite <- (Qplus_0_r b). unfold t. apply Qplus_le_r, Qpos_nonneg. apply Qmin_lb_l. Qed.
imports: QArith.Qround CoRN.metric2.Metric CoRN.metric2.ProductMetric CoRN.metric2.UniformContinuity CoRN.reals.fast.RasterizeQ CoRN.reals.fast.Interval CoRN.metric2.Graph CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax