proposition: Lemma alpha_leq_double i : alpha i.+1 <= a * alpha i.
proof: Proof. apply: isAB_leq_alphaSn; first by apply/isAB_amul/isAB_alpha. by rewrite -[X in X < _]mul1n ltn_mul2r alpha_gt0. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)