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