proposition: Lemma setRaster_uncarry : forall n m (r:raster n m) i j ax ay, raster_well_formed r -> Is_true (RasterIndex (setRaster r true ax ay) i j) -> (Is_true (RasterIndex r i j) \/ (ax, ay) = (i,j)).
proof: Proof. intros. destruct (Nat.eq_dec ax i). - destruct (Nat.eq_dec ay j). right. f_equal; assumption. left. rewrite (setRaster_correct2 r) in H0. exact H0. exact H. right. intro abs. subst j. contradiction. - left. rewrite (setRaster_correct2 r) in H0. exact H0. exact H. left. intro abs. subst i. contradiction. 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