proposition: Lemma eq_fbigmax (e : {fset I}) (F : I -> nat) : 0 < #|`e| -> {i0 : I | i0 \in e /\ \max_(i <- e) F i = F i0}.
proof: Proof. have [n cI] := ubnP #|`e|; elim: n => // n IH e cI in e cI *. rewrite cardfs_gt0 => /diff_fset0_elem[i iH]. have [|H] := leqP #|`(e `\ i)| 0. rewrite leqn0 cardfs_eq0 => /eqP eZ. exists i; split => //. rewrite (big_fsetD1 i) //= eZ big1_fset => [|j]; last by rewrite inE. by apply/maxn_idPl. case: (IH (e `\ i)) => // [|j [jIe jH]]. by move: cI; rewrite (cardfsD1 i) iH. have [FiLFj|FjLFi] := leqP (F i) (F j). exists j; split => //. by move: jIe; rewrite !inE => /andP[]. rewrite (big_fsetD1 i) //= jH. by apply/maxn_idPr. exists i; split. by move: jIe; rewrite !inE => /andP[]. rewrite (big_fsetD1 i) //= jH. by apply/maxn_idPl/ltnW. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)