proposition: Lemma bigfmax_leqP (P : pred I) (m : nat) (e : {fset I}) (F : I -> nat) : reflect (forall i : I, i \in e -> P i -> F i <= m) (\max_(i <- e | P i) F i <= m).
proof: Proof. apply: (iffP idP) => leFm => [i iIe Pi|]. move: leFm. rewrite (big_fsetD1cond _ _ _ Pi) //= => /(leq_trans _)-> //. by apply: leq_maxl. rewrite big_seq_cond. elim/big_ind: _ => //= [m1 m2 m1Lm m2Ln | i /andP[]]. by rewrite geq_max m1Lm. by apply: leFm. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)