proposition: Lemma alphal_neq_nil n : alphal n != nil.
proof: Proof. case: n => //= n. rewrite -size_eq0 size_merge. case: (alphal n) (@gt0_alphal n) => //= c l H. case E : (_ \in _) => //; case : (_ \in _) => //. case: l H E aL1 => // /(_ c); rewrite !inE eqxx => /(_ is_true_true). case: c => // c1 _. by rewrite -{2}[_.+1]mul1n eqn_mul2r /= => /idP/eqP->. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)