proposition: Lemma Vnth_opt_filter_sorted_None A p (ts : vector A p) : forall n (ks : vector nat n), sorted ks -> forall i (hi : i < n), Vnth (Vopt_filter ks ts) hi = None -> forall j (hj : j < n), i < j -> Vnth (Vopt_filter ks ts) hj = None.
proof: Proof. induction ks as [|k n ks]; intros hks i i1 i2 j j1 ij. lia. gen (sorted_cons_elim hks); intro ks_sorted. gen (hks _ i1 _ j1 ij). revert i2. simpl Vopt_filter. rewrite !Vnth_cons. destruct (lt_ge_dec 0 i). intro ai. destruct (lt_ge_dec 0 j). 2: lia. intros _. eapply IHks. hyp. apply ai. lia. assert (i = 0). lia. subst i. clear g. destruct (lt_dec k p). discr. intros _. destruct (lt_ge_dec 0 j). 2: refl. rewrite Vnth_opt_filter. destruct (lt_dec (Vnth ks (Vnth_cons_tail_aux j1 l)) p). lia. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)