proposition: Lemma RasterIndex_in : forall m n i j (r : raster n m), raster_well_formed r -> Is_true (RasterIndex r i j) -> (i < Pos.to_nat m /\ j < Pos.to_nat n)%nat.
proof: Proof. intros. destruct r as [l]. destruct H. rewrite <- H. simpl in H0. clear H m. simpl in H0. revert H0. revert i j. induction l as [|a l]. - intros. exfalso. simpl in H0. destruct i; destruct j; contradiction. - intros. inversion H1. subst l0. subst x. clear H1. specialize (IHl H4). destruct i. + split. apply le_n_S, Nat.le_0_l. apply Vector_bool_in in H0. rewrite <- H3. exact H0. + specialize (IHl i j H0). split. apply le_n_S, IHl. apply IHl. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.raster.Raster CoRN.reals.fast.Interval CoRN.metric2.FinEnum CoRN.metric2.ProductMetric CoRN.logic.Classic