proposition: Fact size_even_poly_exp2n n p : (size p <= 2 ^ n.+1 -> size (even_poly p) <= 2 ^ n)%N.
proof: Proof. move=> Hs; apply: leq_trans (size_even_poly _) _. by rewrite -half_exp2n uphalf_leq. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn