proposition: Lemma size_incr_nth v i : size (incr_nth v i) = if i < size v then size v else i.+1.
proof: Proof. elim: v i => [|n v IHv] [|i] //=; first by rewrite size_ncons /= addn1. by rewrite IHv; apply: fun_if. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)