proposition: Lemma mkseq_nth s : mkseq (nth x0 s) (size s) = s.
proof: Proof. by apply: (@eq_from_nth _ x0); rewrite size_mkseq // => i Hi; rewrite nth_mkseq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)