proposition: Lemma Vnth_replace_neq : forall n i (ip : i < n) j (jp : j < n) (v : vector A n) (a : A), i <> j -> Vnth (Vreplace v ip a) jp = Vnth v jp.
proof: Proof. induction n; intros. lia. VSntac v. destruct i; destruct j; trivial. lia. simpl. rewrite IHn. trivial. lia. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)