proposition: Theorem Plot_correct : @ball (Compact Q2) (proj1_sig (err + Qpos_max ((1 # 2 * n) * w) ((1 # 2 * m) * h))%Qpos) (graphQ (uc_compose clip f)) (Cunit (CentersOfPixels (PixelizeQ2 PlotQ) (l,t) (r,b))).
proof: Proof. apply ball_triangle with (Cunit (approximate (graphQ (uc_compose clip f)) err)). apply ball_approx_r. unfold Compact. rewrite -> ball_Cunit. apply ball_sym. split. apply Qpos_nonneg. apply RasterizeQ2_correct. intros. destruct (InStrengthen H) as [[zx xy] [Hz0 [Hz1 Hz2]]]. simpl in Hz1, Hz2. apply Qball_0 in Hz1. apply Qball_0 in Hz2. rewrite -> Hz1, Hz2. eapply graphQ_bonus. apply Hz0. 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