proposition: Lemma nth_set_nth s n y : nth (set_nth s n y) =1 [eta nth s with n |-> y].
proof: Proof. elim: s n => [|x s IHs] [|n] [|m] //=; rewrite ?nth_nil ?IHs // nth_ncons eqSS. case: ltngtP => // [lt_nm | ->]; last by rewrite subnn. by rewrite nth_default // subn_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)