proposition: Lemma Vsub_replace_l : forall n (v : vector A n) i (h : i<n) x j k (p : j+k<=n), j+k <= i -> Vsub (Vreplace v h x) p = Vsub v p.
proof: Proof. intros. apply Veq_nth; intros. rewrite !Vnth_sub, Vnth_replace_neq. 2: lia. apply Vnth_eq. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)