proposition: Lemma size_subst A n (v : A) s : size (subst n v s) = size s.
proof: Proof. rewrite substE; case: leqP => //=; rewrite size_cat /= size_take size_drop. case: leqP => [sLn|nLs] //= _. by rewrite -subSn // subSS addnC subnK // ltnW. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)