proposition: Lemma nth_pad (T : Type) n (p : T) (s : seq T) i : nth p (pad p n s) i = nth p s i.
proof: Proof. rewrite /pad /= nth_cat. case: (ltnP i (size s)) => //= /(nth_default p) ->. by rewrite nth_nseq if_same. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype