proposition: Lemma nth_update_neq : forall n m l v, n <> m -> nth n (update m v l) = nth n l.
proof: Proof. Proof using. intros n m l. gen n m. induction l; introv N. { rewrite~ update_nil. } { destruct m as [|m']. { rewrite update_zero. do 2 (rewrite nth_pos; [|math]). auto. } { rewrite update_succ. destruct n as [|n']. { rew_listx~. } { rew_listx. applys~ IHl. } } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)