proposition: Lemma uniq_alphal n : uniq (alphal n).
proof: Proof. elim: n => /=[|n IH]. by rewrite !inE negb_or !neq_ltn aL1 aLb /= (ltn_trans aL1). case: (alphal n) (@gt0_alphal n) IH => //= [_ _|c l U /andP[cL uL]]. by rewrite !inE !muln1 neq_ltn aLb. (have [H1|H1] := boolP (_ \in _); have [H2|H2] := boolP (_ \in _); rewrite merge_uniq); rewrite /= ?uL ?andbT //=. - by move: H2; rewrite inE negb_or => /andP[]. - by move: H1; rewrite inE negb_or => /andP[]. move: H1 H2; rewrite !inE !negb_or => /andP[_ ->] /andP[_ ->]. by rewrite eqn_mul2r negb_or !neq_ltn aLb U ?orbT // inE eqxx. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)