proposition: Lemma max_set_nat (e : {fset nat}) : #|`e|.-1 <= \max_(i <- e) i.
proof: Proof. have [n cI] := ubnP #|`e|; elim: n => // [] [|n] IH e cI in e cI *. by move: cI; rewrite ltnS leqn0 => /eqP->. move: cI; rewrite leq_eqVlt => /orP[/eqP eC|]; last first. by apply: IH. have /(eq_fbigmax id)[/= i [iIe iM]] : 0 < #|`e| by rewrite -ltnS eC. have eE : #|` e| = #|` e `\ i|.+1 by rewrite (cardfsD1 i) iIe. have /IH H : #|`e `\ i| < n.+1 by rewrite -eE -ltnS eC. rewrite eE /=. case eIE : (#|` e `\ i|) => [//|k]. have /(eq_fbigmax id)[j []] : 0 < #|` e `\ i| by rewrite eIE. rewrite !inE => /andP[jDi jIe] jM. move: H; rewrite eIE => H. apply: leq_ltn_trans H _; rewrite iM jM. have : j <= i by rewrite -iM; apply: leq_bigfmax. by rewrite leq_eqVlt (negPf jDi). Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)