proposition: Lemma leq_bigfmax (e : {fset I}) (F : I -> nat) i : i \in e -> F i <= \max_(i <- e) F i.
proof: Proof. move=> iIe. have : i \in enum_fset e by []. elim: enum_fset => //= a l IH. rewrite inE big_cons => /orP[/eqP<-|/IH H]; first by apply: leq_maxl. by apply: leq_trans H _; apply: leq_maxr. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)