proposition: Lemma a_lower_bound (k : nat) : 2 ^ (2 ^ k).+1 < a k.+2.
proof: Proof. elim: k => [| k ihk] //. rewrite aS ltnS. have -> : 2 ^ (2 ^ k.+1).+1 = 2 ^ (2 ^ k).+1 * 2 ^ (2 ^ k). by rewrite -expnD addSn addnn -mul2n -expnS. apply: leq_mul; first exact: ltnW. by rewrite -ltnS prednK //; apply: ltn_trans ihk; rewrite ltn_exp2l. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial