proposition: Lemma sorted_cons_elim n k (ks : vector nat n) : sorted (Vcons k ks) -> sorted ks.
proof: Proof. intros h i hi j hj ij. gen (h _ (NatCompat.lt_n_S hi) _ (NatCompat.lt_n_S hj) (NatCompat.lt_n_S ij)). rewrite !Vnth_cons. destruct (lt_ge_dec 0 (S i)); destruct (lt_ge_dec 0 (S j)); try lia. rewrite Vnth_eq with (h2:=hi), Vnth_eq with (h1 := Vnth_cons_tail_aux (NatCompat.lt_n_S hj) l0) (h2:=hj); lia. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)