proposition: Lemma sorted_alphal n : sorted leq (alphal n).
proof: Proof. elim: n => /= [|n IH]; first by rewrite ltnW //= ltnW. apply: merge_sorted; first by apply: leq_total. by do 2 case: (_ \in _) => //=; rewrite leq_mul2r orbC ltnW. by apply: behead_sorted. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)