proposition: Lemma b_in_alphalS n : b * alpha n \in alphal n.+1.
proof: Proof. have := alpha_gt0 n. have := @in_alphal n (b * alpha n). rewrite /alpha /= mem_merge. set h := head _ _. have [H H1 H2|] := boolP (b * _ \in alphal n). apply: H1 => //. by rewrite -{2}[h]mul1n eqn_mul2r negb_or !neq_ltn H2 bL1 !orbT. by have [] := boolP (a * _ \in alphal n); rewrite mem_cat !inE eqxx // orbT. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)