Library prosa.util.minmax


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 37)
  
  T : eqType
  P : pred T
  r : seq T
  F : T -> nat
  i0 : T
  ============================
  i0 \in r -> P i0 -> F i0 <= \max_(i <- r | P i) F i

----------------------------------------------------------------------------- *)


  Proof.
    intros IN0 Pi0; by rewrite (big_rem i0) //= Pi0 leq_maxl.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 54)
  
  ============================
  forall (T : eqType) (i : T) (r : seq_predType T) 
    (P : pred T) (m : nat) (F : T -> nat),
  i \in r -> P i -> m <= F i -> m <= \max_(i0 <- r | P i0) F i0

----------------------------------------------------------------------------- *)


  Proof.
    intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 63)
  
  T : eqType
  i : T
  r : seq_predType T
  P : pred T
  m : nat
  F : T -> nat
  H : i \in r
  H0 : P i
  H1 : m <= F i
  ============================
  m <= \max_(i0 <- r | P i0) F i0

----------------------------------------------------------------------------- *)


    induction r.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 73)
  
  T : eqType
  i : T
  P : pred T
  m : nat
  F : T -> nat
  H : i \in [::]
  H0 : P i
  H1 : m <= F i
  ============================
  m <= \max_(i0 <- [::] | P i0) F i0

subgoal 2 (ID 80) is:
 m <= \max_(i0 <- (a :: r) | P i0) F i0

----------------------------------------------------------------------------- *)


    - by rewrite in_nil in H.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 80)
  
  T : eqType
  i, a : T
  r : seq T
  P : pred T
  m : nat
  F : T -> nat
  H : i \in a :: r
  H0 : P i
  H1 : m <= F i
  IHr : i \in r -> m <= \max_(i <- r | P i) F i
  ============================
  m <= \max_(i0 <- (a :: r) | P i0) F i0

----------------------------------------------------------------------------- *)


      move: H; rewrite in_cons; move ⇒ /orP [/eqP EQA | IN].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 204)
  
  T : eqType
  i, a : T
  r : seq T
  P : pred T
  m : nat
  F : T -> nat
  H0 : P i
  H1 : m <= F i
  IHr : i \in r -> m <= \max_(i <- r | P i) F i
  EQA : i = a
  ============================
  m <= \max_(i0 <- (a :: r) | P i0) F i0

subgoal 2 (ID 205) is:
 m <= \max_(i0 <- (a :: r) | P i0) F i0

----------------------------------------------------------------------------- *)


      {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 204)
  
  T : eqType
  i, a : T
  r : seq T
  P : pred T
  m : nat
  F : T -> nat
  H0 : P i
  H1 : m <= F i
  IHr : i \in r -> m <= \max_(i <- r | P i) F i
  EQA : i = a
  ============================
  m <= \max_(i0 <- (a :: r) | P i0) F i0

----------------------------------------------------------------------------- *)


        clear IHr; subst a.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 208)
  
  T : eqType
  i : T
  r : seq T
  P : pred T
  m : nat
  F : T -> nat
  H0 : P i
  H1 : m <= F i
  ============================
  m <= \max_(i0 <- (i :: r) | P i0) F i0

----------------------------------------------------------------------------- *)


        rewrite (big_rem i) //=; last by rewrite in_cons; apply/orP; left.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 226)
  
  T : eqType
  i : T
  r : seq T
  P : pred T
  m : nat
  F : T -> nat
  H0 : P i
  H1 : m <= F i
  ============================
  m <=
  maxn (if P i then F i else 0)
    (\max_(y <- (if i == i then r else i :: rem (T:=T) i r) | P y) F y)

----------------------------------------------------------------------------- *)


        apply leq_trans with (F i); first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 305)
  
  T : eqType
  i : T
  r : seq T
  P : pred T
  m : nat
  F : T -> nat
  H0 : P i
  H1 : m <= F i
  ============================
  F i <=
  maxn (if P i then F i else 0)
    (\max_(y <- (if i == i then r else i :: rem (T:=T) i r) | P y) F y)

----------------------------------------------------------------------------- *)


          by rewrite H0 leq_maxl.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 205)

subgoal 1 (ID 205) is:
 m <= \max_(i0 <- (a :: r) | P i0) F i0

----------------------------------------------------------------------------- *)


      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 205)
  
  T : eqType
  i, a : T
  r : seq T
  P : pred T
  m : nat
  F : T -> nat
  H0 : P i
  H1 : m <= F i
  IHr : i \in r -> m <= \max_(i <- r | P i) F i
  IN : i \in r
  ============================
  m <= \max_(i0 <- (a :: r) | P i0) F i0

----------------------------------------------------------------------------- *)


      {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 205)
  
  T : eqType
  i, a : T
  r : seq T
  P : pred T
  m : nat
  F : T -> nat
  H0 : P i
  H1 : m <= F i
  IHr : i \in r -> m <= \max_(i <- r | P i) F i
  IN : i \in r
  ============================
  m <= \max_(i0 <- (a :: r) | P i0) F i0

----------------------------------------------------------------------------- *)


        apply leq_trans with (\max_(i0 <- r | P i0) F i0); first by apply IHr.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 318)
  
  T : eqType
  i, a : T
  r : seq T
  P : pred T
  m : nat
  F : T -> nat
  H0 : P i
  H1 : m <= F i
  IHr : i \in r -> m <= \max_(i <- r | P i) F i
  IN : i \in r
  ============================
  \max_(i0 <- r | P i0) F i0 <= \max_(i0 <- (a :: r) | P i0) F i0

----------------------------------------------------------------------------- *)


        rewrite [in X in _ X](big_rem a) //=; last by rewrite in_cons; apply/orP; left.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 342)
  
  T : eqType
  i, a : T
  r : seq T
  P : pred T
  m : nat
  F : T -> nat
  H0 : P i
  H1 : m <= F i
  IHr : i \in r -> m <= \max_(i <- r | P i) F i
  IN : i \in r
  ============================
  \max_(i0 <- r | P i0) F i0 <=
  maxn (if P a then F a else 0)
    (\max_(y <- (if a == a then r else a :: rem (T:=T) a r) | P y) F y)

----------------------------------------------------------------------------- *)


        have Ob: a == a; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 423)
  
  T : eqType
  i, a : T
  r : seq T
  P : pred T
  m : nat
  F : T -> nat
  H0 : P i
  H1 : m <= F i
  IHr : i \in r -> m <= \max_(i <- r | P i) F i
  IN : i \in r
  Ob : a == a
  ============================
  \max_(i0 <- r | P i0) F i0 <=
  maxn (if P a then F a else 0)
    (\max_(y <- (if a == a then r else a :: rem (T:=T) a r) | P y) F y)

----------------------------------------------------------------------------- *)


          by rewrite Ob leq_maxr.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


      }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

  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).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 75)
  
  T : eqType
  P : pred T
  r : seq T
  F : T -> nat
  m : nat
  ============================
  reflect (forall i : T, i \in r -> P i -> F i <= m)
    (\max_(i <- r | P i) F i <= m)

----------------------------------------------------------------------------- *)


  Proof.
    apply: (iffP idP) ⇒ leFm ⇒ [i IINR Pi|];
      first by apply: leq_trans leFm; apply leq_bigmax_cond_seq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 110)
  
  T : eqType
  P : pred T
  r : seq T
  F : T -> nat
  m : nat
  leFm : forall i : T, i \in r -> P i -> F i <= m
  ============================
  \max_(i <- r | P i) F i <= m

----------------------------------------------------------------------------- *)


    rewrite big_seq_cond; elim/big_ind: _ ⇒ // m1 m2.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 232)
  
  T : eqType
  P : pred T
  r : seq T
  F : T -> nat
  m : nat
  leFm : forall i : T, i \in r -> P i -> F i <= m
  m1, m2 : nat
  ============================
  m1 <= m -> m2 <= m -> maxn m1 m2 <= m

subgoal 2 (ID 233) is:
 F m1 <= m

----------------------------------------------------------------------------- *)


      by intros; rewrite geq_max; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 233)
  
  T : eqType
  P : pred T
  r : seq T
  F : T -> nat
  m : nat
  leFm : forall i : T, i \in r -> P i -> F i <= m
  m1 : T
  m2 : (m1 \in r) && P m1
  ============================
  F m1 <= m

----------------------------------------------------------------------------- *)


      by move: m2 ⇒ /andP [M1IN Pm1]; apply: leFm.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 103)
  
  T : eqType
  P : pred T
  r : seq T
  F1, F2 : T -> nat
  ============================
  (forall i : T, i \in r -> P i -> F1 i <= F2 i) ->
  \max_(i <- r | P i) F1 i <= \max_(i <- r | P i) F2 i

----------------------------------------------------------------------------- *)


  Proof.
    intros; apply /bigmax_leq_seqP; intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 138)
  
  T : eqType
  P : pred T
  r : seq T
  F1, F2 : T -> nat
  H : forall i : T, i \in r -> P i -> F1 i <= F2 i
  i : T
  H0 : i \in r
  H1 : P i
  ============================
  F1 i <= \max_(i0 <- r | P i0) F2 i0

----------------------------------------------------------------------------- *)


    specialize (H i); feed_n 2 H; try(done).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 152)
  
  T : eqType
  P : pred T
  r : seq T
  F1, F2 : T -> nat
  i : T
  H : F1 i <= F2 i
  H0 : i \in r
  H1 : P i
  ============================
  F1 i <= \max_(i0 <- r | P i0) F2 i0

----------------------------------------------------------------------------- *)


    rewrite (big_rem i) //=; rewrite H1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 216)
  
  T : eqType
  P : pred T
  r : seq T
  F1, F2 : T -> nat
  i : T
  H : F1 i <= F2 i
  H0 : i \in r
  H1 : P i
  ============================
  F1 i <= maxn (F2 i) (\max_(y <- rem (T:=T) i r | P y) F2 y)

----------------------------------------------------------------------------- *)


      by apply leq_trans with (F2 i); [ | rewrite leq_maxl].

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

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

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 113)
  
  n : nat
  ============================
  0 < n -> \max_(i < n) i < n

----------------------------------------------------------------------------- *)


  Proof.
    intros LT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 114)
  
  n : nat
  LT : 0 < n
  ============================
  \max_(i < n) i < n

----------------------------------------------------------------------------- *)


    destruct n; first by rewrite ltn0 in LT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 125)
  
  n : nat
  LT : 0 < n.+1
  ============================
  \max_(i < n.+1) i < n.+1

----------------------------------------------------------------------------- *)


    clear LT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 137)
  
  n : nat
  ============================
  \max_(i < n.+1) i < n.+1

----------------------------------------------------------------------------- *)


    induction n; first by rewrite big_ord_recr /= big_ord0 maxn0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 144)
  
  n : nat
  IHn : \max_(i < n.+1) i < n.+1
  ============================
  \max_(i < n.+2) i < n.+2

----------------------------------------------------------------------------- *)


    rewrite big_ord_recr /=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 172)
  
  n : nat
  IHn : \max_(i < n.+1) i < n.+1
  ============================
  maxn (\max_(i < n.+1) i) n.+1 < n.+2

----------------------------------------------------------------------------- *)


      by unfold maxn at 1; rewrite IHn.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

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

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 125)
  
  n : nat
  P : pred nat
  i0 : 'I_n
  ============================
  P i0 -> \max_(i < n | P i) i < n

----------------------------------------------------------------------------- *)


  Proof.
    intros LT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 126)
  
  n : nat
  P : pred nat
  i0 : 'I_n
  LT : P i0
  ============================
  \max_(i < n | P i) i < n

----------------------------------------------------------------------------- *)


    destruct n; first by destruct i0 as [i0 P0]; move: (P0) ⇒ P0'; rewrite ltn0 in P0'.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 142)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  LT : P i0
  ============================
  \max_(i < n.+1 | P i) i < n.+1

----------------------------------------------------------------------------- *)


    rewrite big_mkcond.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 176)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  LT : P i0
  ============================
  \big[maxn_monoid/0]_i (if P i then i else 0) < n.+1

----------------------------------------------------------------------------- *)


    apply leq_ltn_trans with (n := \max_(i < n.+1) i).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 184)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  LT : P i0
  ============================
  \big[maxn_monoid/0]_i (if P i then i else 0) <= \max_(i < n.+1) i

subgoal 2 (ID 185) is:
 \max_(i < n.+1) i < n.+1

----------------------------------------------------------------------------- *)


    {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 184)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  LT : P i0
  ============================
  \big[maxn_monoid/0]_i (if P i then i else 0) <= \max_(i < n.+1) i

----------------------------------------------------------------------------- *)


      apply/bigmax_leqP; ins.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 243)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  LT : P i0
  i : 'I_n.+1
  H : true
  ============================
  (if P i then i else 0) <= \max_(i1 < n.+1) i1

----------------------------------------------------------------------------- *)


      destruct (P i); last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 250)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  LT : P i0
  i : 'I_n.+1
  H : true
  ============================
  i <= \max_(i1 < n.+1) i1

----------------------------------------------------------------------------- *)


      by apply leq_bigmax_cond.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 185)

subgoal 1 (ID 185) is:
 \max_(i < n.+1) i < n.+1

----------------------------------------------------------------------------- *)


    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 185)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  LT : P i0
  ============================
  \max_(i < n.+1) i < n.+1

----------------------------------------------------------------------------- *)


    by apply bigmax_ord_ltn_identity.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

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

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 137)
  
  n : nat
  P : pred nat
  i0 : 'I_n
  ============================
  P i0 -> P (\max_(i < n | P i) i)

----------------------------------------------------------------------------- *)


  Proof.
    intros PRED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 138)
  
  n : nat
  P : pred nat
  i0 : 'I_n
  PRED : P i0
  ============================
  P (\max_(i < n | P i) i)

----------------------------------------------------------------------------- *)


    induction n.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 150)
  
  P : pred nat
  i0 : 'I_0
  PRED : P i0
  ============================
  P (\max_(i < 0 | P i) i)

subgoal 2 (ID 157) is:
 P (\max_(i < n.+1 | P i) i)

----------------------------------------------------------------------------- *)


    {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 150)
  
  P : pred nat
  i0 : 'I_0
  PRED : P i0
  ============================
  P (\max_(i < 0 | P i) i)

----------------------------------------------------------------------------- *)


      destruct i0 as [i0 P0].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 165)
  
  P : pred nat
  i0 : nat
  P0 : i0 < 0
  PRED : P (Ordinal (n:=0) (m:=i0) P0)
  ============================
  P (\max_(i < 0 | P i) i)

----------------------------------------------------------------------------- *)


      by move: (P0) ⇒ P1; rewrite ltn0 in P1.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 157)

subgoal 1 (ID 157) is:
 P (\max_(i < n.+1 | P i) i)

----------------------------------------------------------------------------- *)


    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 157)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  PRED : P i0
  IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
  ============================
  P (\max_(i < n.+1 | P i) i)

----------------------------------------------------------------------------- *)


    rewrite big_mkcond big_ord_recr /=.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 221)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  PRED : P i0
  IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
  ============================
  P (maxn (\max_(i < n) (if P i then i else 0)) (if P n then n else 0))

----------------------------------------------------------------------------- *)


destruct (P n) eqn:Pn.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 233)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  PRED : P i0
  IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
  Pn : P n = true
  ============================
  P (maxn (\max_(i < n) (if P i then i else 0)) n)

subgoal 2 (ID 234) is:
 P (maxn (\max_(i < n) (if P i then i else 0)) 0)

----------------------------------------------------------------------------- *)


    {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 233)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  PRED : P i0
  IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
  Pn : P n = true
  ============================
  P (maxn (\max_(i < n) (if P i then i else 0)) n)

----------------------------------------------------------------------------- *)


      destruct n; first by rewrite big_ord0 maxn0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 258)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+2
  PRED : P i0
  IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
  Pn : P n.+1 = true
  ============================
  P (maxn (\max_(i < n.+1) (if P i then i else 0)) n.+1)

----------------------------------------------------------------------------- *)


      unfold maxn at 1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 272)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+2
  PRED : P i0
  IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
  Pn : P n.+1 = true
  ============================
  P
    (if \max_(i < n.+1) (if P i then i else 0) < n.+1
     then n.+1
     else \max_(i < n.+1) (if P i then i else 0))

----------------------------------------------------------------------------- *)


      destruct (\max_(i < n.+1) (match P (@nat_of_ord (S n) i) return nat with
                    | true ⇒ @nat_of_ord (S n) i
                    | falseO
                                 end) < n.+1) eqn:Pi; first by rewrite Pi.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 290)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+2
  PRED : P i0
  IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
  Pn : P n.+1 = true
  Pi : (\max_(i < n.+1) (if P i then i else 0) < n.+1) = false
  ============================
  P
    (if \max_(i < n.+1) (if P i then i else 0) < n.+1
     then n.+1
     else \max_(i < n.+1) (if P i then i else 0))

----------------------------------------------------------------------------- *)


      exfalso.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 293)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+2
  PRED : P i0
  IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
  Pn : P n.+1 = true
  Pi : (\max_(i < n.+1) (if P i then i else 0) < n.+1) = false
  ============================
  False

----------------------------------------------------------------------------- *)


      apply negbT in Pi; move: Pi ⇒ /negP BUG.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 323)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+2
  PRED : P i0
  IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
  Pn : P n.+1 = true
  BUG : ~ \max_(i < n.+1) (if P i then i else 0) < n.+1
  ============================
  False

----------------------------------------------------------------------------- *)


      apply BUG.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 324)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+2
  PRED : P i0
  IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
  Pn : P n.+1 = true
  BUG : ~ \max_(i < n.+1) (if P i then i else 0) < n.+1
  ============================
  \max_(i < n.+1) (if P i then i else 0) < n.+1

----------------------------------------------------------------------------- *)


      apply leq_ltn_trans with (n := \max_(i < n.+1) i).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 332)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+2
  PRED : P i0
  IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
  Pn : P n.+1 = true
  BUG : ~ \max_(i < n.+1) (if P i then i else 0) < n.+1
  ============================
  \max_(i < n.+1) (if P i then i else 0) <= \max_(i < n.+1) i

subgoal 2 (ID 333) is:
 \max_(i < n.+1) i < n.+1

----------------------------------------------------------------------------- *)


      {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 332)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+2
  PRED : P i0
  IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
  Pn : P n.+1 = true
  BUG : ~ \max_(i < n.+1) (if P i then i else 0) < n.+1
  ============================
  \max_(i < n.+1) (if P i then i else 0) <= \max_(i < n.+1) i

----------------------------------------------------------------------------- *)


        apply/bigmax_leqP; ins.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 392)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+2
  PRED : P i0
  IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
  Pn : P n.+1 = true
  BUG : ~ \max_(i < n.+1) (if P i then i else 0) < n.+1
  i : 'I_n.+1
  H : true
  ============================
  (if P i then i else 0) <= \max_(i1 < n.+1) i1

----------------------------------------------------------------------------- *)


        destruct (P i); last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 399)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+2
  PRED : P i0
  IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
  Pn : P n.+1 = true
  BUG : ~ \max_(i < n.+1) (if P i then i else 0) < n.+1
  i : 'I_n.+1
  H : true
  ============================
  i <= \max_(i1 < n.+1) i1

----------------------------------------------------------------------------- *)


        by apply leq_bigmax_cond.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 333)

subgoal 1 (ID 333) is:
 \max_(i < n.+1) i < n.+1
subgoal 2 (ID 234) is:
 P (maxn (\max_(i < n) (if P i then i else 0)) 0)

----------------------------------------------------------------------------- *)


      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 333)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+2
  PRED : P i0
  IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
  Pn : P n.+1 = true
  BUG : ~ \max_(i < n.+1) (if P i then i else 0) < n.+1
  ============================
  \max_(i < n.+1) i < n.+1

----------------------------------------------------------------------------- *)


      by apply bigmax_ord_ltn_identity.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 234)

subgoal 1 (ID 234) is:
 P (maxn (\max_(i < n) (if P i then i else 0)) 0)

----------------------------------------------------------------------------- *)


    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 234)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  PRED : P i0
  IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
  Pn : P n = false
  ============================
  P (maxn (\max_(i < n) (if P i then i else 0)) 0)

----------------------------------------------------------------------------- *)


    {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 234)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  PRED : P i0
  IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
  Pn : P n = false
  ============================
  P (maxn (\max_(i < n) (if P i then i else 0)) 0)

----------------------------------------------------------------------------- *)


      rewrite maxn0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 407)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  PRED : P i0
  IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
  Pn : P n = false
  ============================
  P (\max_(i < n) (if P i then i else 0))

----------------------------------------------------------------------------- *)


      rewrite -big_mkcond /=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 417)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  PRED : P i0
  IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
  Pn : P n = false
  ============================
  P (\max_(i < n | P i) i)

----------------------------------------------------------------------------- *)


      have LT: i0 < n.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 418)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  PRED : P i0
  IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
  Pn : P n = false
  ============================
  i0 < n

subgoal 2 (ID 420) is:
 P (\max_(i < n | P i) i)

----------------------------------------------------------------------------- *)


      {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 418)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  PRED : P i0
  IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
  Pn : P n = false
  ============================
  i0 < n

----------------------------------------------------------------------------- *)


        rewrite ltn_neqAle; apply/andP; split;
          last by rewrite -ltnS; apply ltn_ord.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 450)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  PRED : P i0
  IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
  Pn : P n = false
  ============================
  i0 != n

----------------------------------------------------------------------------- *)


        apply/negP; move ⇒ /eqP BUG.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 510)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  PRED : P i0
  IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
  Pn : P n = false
  BUG : i0 = n
  ============================
  False

----------------------------------------------------------------------------- *)


        by rewrite -BUG PRED in Pn.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 420)

subgoal 1 (ID 420) is:
 P (\max_(i < n | P i) i)

----------------------------------------------------------------------------- *)


      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 420)
  
  n : nat
  P : pred nat
  i0 : 'I_n.+1
  PRED : P i0
  IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
  Pn : P n = false
  LT : i0 < n
  ============================
  P (\max_(i < n | P i) i)

----------------------------------------------------------------------------- *)


      by rewrite (IHn (Ordinal LT)).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

End ExtraLemmas.