proposition: Lemma PlotSubset_fix_blank : forall (A : CR*CR -> Prop) (x y : CR) (i j n m:nat) (ltin : (i < n)%nat) (ltjm : (j < m)%nat) (b r stepX stepY:Q) (d e:Q) (ltde : d < e) (loc : LocatedSubset (ProductMS CR CR) A), ball d x (inject_Q_CR (r - inject_Z (Z.of_nat (n-i)) * stepX)%Q) -> ball d y (inject_Q_CR (b + inject_Z (Z.of_nat (m-j)) * stepY)%Q) -> nth i (nth j (PlotSubset_fix A n m b r stepX stepY d e ltde loc) nil) false = false -> ~A (x,y).
proof: Proof. induction j. - intros. intro abs. destruct m. exfalso; inversion ltjm. simpl in H1. refine (PlotLine_blank A i n ltin r stepX x (' (b + inject_Z (Z.pos (Pos.of_succ_nat m)) * stepY)%Q)%CR y d e ltde loc H _ H1 abs). apply ball_sym. exact H0. - intros. intro abs. destruct m. inversion ltjm. simpl in H1. apply (IHj n m ltin (proj2 (Nat.succ_lt_mono j m) ltjm) b r stepX stepY d e ltde loc H H0 H1 abs). 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