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.