proposition: Lemma nth_error_set_nth_other m n a b : m != n -> nth_error st m = Some a -> nth_error (set_nth def st n b) m = Some a.
proof: Proof. elim: m st n => [|m IH] [|c st'] [|n] //=; rewrite eqSS => *; exact: IH. Qed.
imports: mathcomp(all_ssreflect)