proposition: Lemma substE A n (v : A) s : subst n v s = if n < size s then take n s ++ (v :: drop n.+1 s) else s.
proof: Proof. elim: n s => /= [[|a s]|/= n IH [|a s]] //=; first by rewrite drop0. by rewrite {}IH ltnS; case: leqP. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)