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