Library probsa.util.min

Require Export Reals.
From mathcomp Require Export ssreflect ssrnat ssrbool seq.

Definition min_option (xs : seq nat) : option nat :=
  match xs with
  | [::] ⇒ None
  | h::tl ⇒ Some (foldl minn h tl)
  end.

Definition min_default (d : nat) (xs : seq nat) : nat := foldl minn d xs.
Definition min1 (xs : seq R) : R := foldl Rmin 1%R xs.

Lemma min1_cons :
  ∀ xs x0,
    min1 (x0 :: xs) = Rmin x0 (min1 xs).

Lemma Rle_min_compat :
  ∀ (x y z w : R),
    (x ≤ z)%R →
    (y ≤ w)%R →
    (Rmin x y ≤ Rmin z w)%R.