proposition: Lemma bigmax_leq_pointwise (I :finType) (P : pred I) (F G : I -> nat) : {in P, forall x, F x <= G x} -> \max_(i | P i) F i <= \max_(i | P i) G i.
proof: Proof. move => ?. elim/big_ind2 : _ => // y1 y2 x1 x2 A B. by rewrite geq_max !leq_max A B orbT. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)