proposition: Lemma PlotLine_blank : forall (A : CR*CR -> Prop) (n i:nat) (ltni : (n < i)%nat) (r step:Q) (x y z : CR) (d e:Q) (ltde : d < e) (loc : LocatedSubset (ProductMS CR CR) A), ball d x (inject_Q_CR (r - inject_Z (Z.of_nat (i-n)) * step)%Q) -> ball d y z -> nth n (PlotLine A i r step y d e ltde loc) false = false -> ~A (x,z).
proof: Proof. induction n. - intros. intro abs. destruct i. exfalso; inversion ltni. simpl in H1. destruct (loc d e (@pair (@RegularFunction Q Qball) (@RegularFunction Q Qball) (inject_Q_CR (Qminus r (Qmult (inject_Z (Zpos (Pos.of_succ_nat i))) step))) y) ltde). 2: discriminate. clear H1. specialize (n (x,z) abs). contradict n. split. + unfold fst. apply ball_sym. exact H. + exact H0. - intros. intro abs. destruct i. inversion ltni. simpl in H1. revert abs. refine (IHn i (proj2 (Nat.succ_lt_mono n i) ltni) r step x y z d e ltde loc _ H0 H1). replace (i-n)%nat with (S i - S n)%nat by reflexivity. exact H. 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