proposition: Lemma a_lower_boundW (k : nat) : 2 ^ 2 ^ k <= a k.+2.
proof: Proof. by apply: ltnW; apply: ltn_trans (a_lower_bound _); rewrite ltn_exp2l. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial