proposition: Lemma S1E : S_[1] =1 S1.
proof: Proof. case => [|i]. by rewrite /dsum_alphaL /conv /= dsum_alpha_0. rewrite S1_bigmin /dsum_alphaL /conv /= subnn addn0 -S1_bigmin. rewrite (_ : \min_(_ <= _) _ = S1 i.+1). by rewrite (minn_idPr _) // -addnn leq_addr. by rewrite S1_bigmin; apply: bigmin_ext => i1 i1H; rewrite mul1n. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)