proposition: Lemma head_pad (T : Type) n (p : T) (s : seq T) : head p (pad p n s) = head p s.
proof: Proof. by elim: s => [| s0 s IHs] //=; rewrite subn0; case: n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype