proposition: Lemma RasterizeQ2_in_recip : forall (points : list (Z*Z)) (i j : nat) n m (r:raster n m), raster_well_formed r -> Is_true (RasterIndex (fold_left (fun (rast:raster n m) (p:Z*Z) => setRaster rast true (Z.to_nat (fst p)) (Z.to_nat (snd p))) points r) i j) -> (In (i, j) (map (fun p => (Z.to_nat (fst p), Z.to_nat (snd p))) points) \/ Is_true (RasterIndex r i j)).
proof: Proof. induction points as [|[ax ay] points]. - intros. right. exact H0. - intros. simpl in H0. destruct (RasterIndex r i j) eqn:des. right. reflexivity. left. destruct (IHpoints i j n m (setRaster r true (Z.to_nat ax) (Z.to_nat ay)) ). apply setRaster_wf, H. exact H0. right. exact H1. destruct (Nat.eq_dec (Z.to_nat ax) i). + destruct (Nat.eq_dec (Z.to_nat ay) j). left. f_equal; assumption. exfalso. apply setRaster_uncarry in H1. destruct H1. unfold Is_true in H1. rewrite des in H1. contradiction. inversion H1. contradiction. exact H. + exfalso. apply setRaster_uncarry in H1. destruct H1. unfold Is_true in H1. rewrite des in H1. contradiction. inversion H1. contradiction. exact H. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.RasterQ CoRN.reals.fast.Interval CoRN.logic.Classic CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs Coq.QArith.Qround