proposition: Lemma PlotRadiusInc : forall n m t l b r, l < r -> (1#2) * PlotRadius n m t l b r < PlotRadius n m t l b r.
proof: Proof. intros. rewrite <- (Qmult_1_l (PlotRadius n m t l b r)) at 2. apply Qmult_lt_r. 2: reflexivity. apply (Qlt_le_trans _ ((r-l) * (1#n))%Q). apply Qlt_minus_iff in H. apply (Qpos_ispos (exist _ _ H * (1 # n))). apply Qmax_ub_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