proposition: Lemma size_bottom n p : (size (bottom n p) <= 2 ^ n)%N.
proof: Proof. elim: n p => /= [|n IH] p; first by apply: size_polyC_leq1. apply: leq_trans (size_add _ _) _. rewrite geq_max (leq_trans (IH _)) //=; last by rewrite leq_exp2l. apply: leq_trans (size_mul_leq _ _) _. by rewrite size_polyXn expnS mul2n -addnn leq_add. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum)