proposition: Lemma PlotSubset_blank : forall {A : CR*CR -> Prop} (i j : nat) (n m : positive) (t l b r : Q) (x y : CR) (ltin : (i < Pos.to_nat n)%nat) (ltjm : (j < Pos.to_nat m)%nat) (ltlr : l < r) (loc : LocatedSubset (ProductMS CR CR) A), RasterIndex (PlotSubset n m t l b r ltlr loc) j i = false -> let stepX := ((r-l) * (1#n))%Q in let stepY := ((t-b) * (1#m))%Q in ball ((1#2)*(Qmax stepX stepY)) x (inject_Q_CR (l + (inject_Z (Z.of_nat i) + (1#2)) * stepX)%Q) -> ball ((1#2)*(Qmax stepX stepY)) y (inject_Q_CR (t - (inject_Z (Z.of_nat j) + (1#2)) * stepY)%Q) -> ~A (x,y).
proof: Proof. intros. setoid_replace (l + (inject_Z (Z.of_nat i)+(1#2)) * stepX)%Q with ((r + (1#2)*stepX) - inject_Z (Z.of_nat (Pos.to_nat n - i)) * stepX)%Q in H0. setoid_replace (t - (inject_Z (Z.of_nat j) + (1#2)) * stepY)%Q with ((b-(1#2)*stepY) + inject_Z (Z.of_nat (Pos.to_nat m - j)) * stepY)%Q in H1. exact (PlotSubset_fix_blank A x y i j (Pos.to_nat n) (Pos.to_nat m) ltin ltjm _ _ stepX stepY ((1#2)*(Qmax stepX stepY)) (Qmax stepX stepY) (PlotRadiusInc n m t l b r ltlr) loc H0 H1 H). - unfold canonical_names.equiv, stdlib_rationals.Q_eq. rewrite Nat2Z.inj_sub. unfold Zminus. rewrite Q.Zplus_Qplus, inject_Z_opp. rewrite <- (Qplus_inj_r _ _ ((inject_Z (Z.of_nat j)+(1#2)) * stepY)). ring_simplify. rewrite positive_nat_Z. unfold stepY. rewrite <- Qmult_assoc. setoid_replace ((1 # m) * inject_Z (Z.pos m)) with 1%Q by reflexivity. rewrite Qmult_1_r. ring. apply (Nat.le_trans _ (S j)). apply le_S, Nat.le_refl. exact ltjm. - unfold canonical_names.equiv, stdlib_rationals.Q_eq. rewrite Nat2Z.inj_sub. unfold Zminus. rewrite Q.Zplus_Qplus, inject_Z_opp. rewrite positive_nat_Z. rewrite <- (Qplus_inj_r _ _ (stepX * inject_Z (Z.pos n) -inject_Z (Z.of_nat i) * stepX - (1#2)*stepX)). ring_simplify. unfold stepX. rewrite <- Qmult_assoc. setoid_replace ((1 # n) * inject_Z (Z.pos n)) with 1%Q by reflexivity. rewrite Qmult_1_r. ring. apply (Nat.le_trans _ (S i)). apply le_S, Nat.le_refl. exact ltin. 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