proposition: Lemma Vector_bool_in : forall (v : list bool) j, Is_true (nth j v false) -> (j < length v)%nat.
proof: Proof. induction v. - intros j H. destruct j; contradiction H. - intros j H. simpl in H. destruct j. apply le_n_S, Nat.le_0_l. simpl. apply le_n_S, IHv, H. 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