proposition: Lemma size_set_nth s n y : size (set_nth s n y) = maxn n.+1 (size s).
proof: Proof. rewrite maxnC; elim: s n => [|x s IHs] [|n] //=. - by rewrite size_ncons addn1. - by rewrite IHs maxnSS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)