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