proposition: Lemma dsum_alpha3_S n : S_[1] n.+1 = (S_[3] n).+1.
proof: Proof. rewrite S1E. have := dsum_alphal_min_3 1 n. rewrite S1E addn1 /minn; case: leqP => // _ /eqP. rewrite -addnn -{1}[S1 _]add0n eqn_add2r. suff : 0 < S1 n.+1 by case: S1. rewrite -dsum_alpha_1 increasingE //. by apply: increasing_dsum_alpha. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)