Library prosa.util.minmax

Require Export prosa.util.notation prosa.util.nat prosa.util.list.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

(* Additional lemmas about max. *)
Section ExtraLemmas.

  Lemma leq_bigmax_cond_seq (T : eqType) (P : pred T) (r : seq T) F i0 :
    i0 \in r P i0 F i0 \max_(i <- r | P i) F i.

  Lemma bigmax_sup_seq:
     (T: eqType) (i: T) r (P: pred T) m F,
      i \in r P i m F i m \max_(i <- r| P i) F i.

  Lemma bigmax_leq_seqP (T : eqType) (P : pred T) (r : seq T) F m :
    reflect ( i, i \in r P i F i m)
            (\max_(i <- r | P i) F i m).

  Lemma leq_big_max (T : eqType) (P : pred T) (r : seq T) F1 F2 :
    ( i, i \in r P i F1 i F2 i)
    \max_(i <- r | P i) F1 i \max_(i <- r | P i) F2 i.

  Lemma bigmax_ord_ltn_identity n :
    n > 0
    \max_(i < n) i < n.

  Lemma bigmax_ltn_ord n (P : pred nat) (i0: 'I_n) :
    P i0
    \max_(i < n | P i) i < n.

  Lemma bigmax_pred n (P : pred nat) (i0: 'I_n) :
    P (i0)
    P (\max_(i < n | P i) i).

End ExtraLemmas.