proposition: Lemma set_set_nth s n1 y1 n2 y2 (s2 := set_nth s n2 y2) : set_nth (set_nth s n1 y1) n2 y2 = if n1 == n2 then s2 else set_nth s2 n1 y1.
proof: Proof. have [-> | ne_n12] := eqVneq. apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnA maxnn. by do 2!rewrite !nth_set_nth /=; case: eqP. apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnCA. by do 2!rewrite !nth_set_nth /=; case: eqP => // ->; case: eqVneq ne_n12. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)