proposition: Lemma alpha4_small : ((α_[4] 0 = 2) * (α_[4] 1 = 4) * (α_[4] 2 = 4) * (α_[4] 3 = 6) * ( α_[4] 4 = 8) * (α_[4] 5 = 12))%type.
proof: Proof. by rewrite /alphaL /delta !S4_small; compute. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)