proposition: Lemma S4_small : ((S_[4] 0 = 0) * (S_[4] 1 = 2) * (S_[4] 2 = 6) * (S_[4] 3 = 10) * ( S_[4] 4 = 16) * (S_[4] 5 = 24) * (S_[4] 6 = 36))%type.
proof: Proof. by rewrite /dsum_alphaL /conv /= /dsum_alpha -!(big_mkord xpredT) unlock /=; compute. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)