fact: Definition PlotRadius (n m : positive) (t l b r : Q) : Q := Qmax ((r-l) * (1#n))%Q ((t-b) * (1#m))%Q.
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