proposition: Lemma In_filtered_list : forall (l : list Q) (q : Q) (filterList : list bool) (j : nat), (length filterList <= length l)%nat -> Is_true (nth j filterList false) -> In (nth j l q) (map fst (filter snd (combine l filterList))).
proof: Proof. induction l. - intros. destruct filterList. 2: exfalso; inversion H. exfalso. simpl in H0. destruct j; contradiction. - intros. destruct filterList. destruct j; contradiction. simpl in H. apply le_S_n in H. simpl. destruct j. + simpl in H0. destruct b. 2: contradiction. left. reflexivity. + destruct b. right. exact (IHl q _ _ H H0). exact (IHl q _ _ H H0). 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