proposition: Lemma Vnth_cons : forall x n (v : vector A n) i (h1:i<S n), Vnth (Vcons x v) h1 = match lt_ge_dec 0 i with | left h2 => Vnth v (Vnth_cons_tail_aux h1 h2) | _ => x end.
proof: Proof. intros. case (lt_ge_dec 0 i); intro. apply Vnth_cons_tail. apply Vnth_cons_head. lia. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)