proposition: Lemma size_algo n p : (size (algo n p) <= 2 ^ n)%N.
proof: Proof. elim: n p => /= [|n IH] p; first by rewrite size_polyC; case: eqP. by apply: size_merge; apply: IH. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum)