fact: Fixpoint alphal (n : nat) := if n isn't n1.+1 then [:: 1; a; b] else let l := alphal n1 in merge leq (let c := head 1 l in let l1 := if b * c \in l then [::] else [:: b * c] in if a * c \in l then l1 else a * c :: l1) (behead l).
imports: mathcomp(all_ssreflect finmap) hanoi(extra)