Library Subsets.ord_compl

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Additional definitions and results about ordinals.

Description

Given n : nat, let us recall that 'I_n, ie ordinal n, is the finite type of natural numbers (strictly) smaller than n. Its cardinal is n. It is defined in ssreflect.fintype in the Mathematical Components library.

Additional notations

  • 'I_{m,n} is for 'I_m 'I_n;
  • 'I_[n] is for 'I_{n,n};
  • 'I_{m,n,p} is for 'I_m 'I_{n,p}.

Changes from the Mathematical Components library

  • ord1 is renamed I_1_is_unit.
  • The new ord1 is the ordinal of value 1, when the bound is (strictly) larger than 1.

Support for specific ordinal transformations

Naming rules:
  • the results used to define <transf> are called <transf>*_proof;
  • most transformations are called <op>_ord;
  • some specializations for successor are called <op>_S;
  • <op>_ord is used to define <op>F in Finite_family;
  • <op>_S is used to define <op>F_S in Finite_family.
Some conventions for the sequel:
  • n..p means all integers from n to p;
  • [n.. and ..n] means included the bound n;
  • (n.. and ..n) means excluded the bound n;
  • n..i^..p means all integers from n to p, except i.
  • widen_S is the canonical injection from 'I_n to 'I_n.+1. It maps [0..n) ⊂ 'I_n into [0..n) ⊂ 'I_n.+1.
  • narrow_S is the canonical projection from 'I_n.+1 onto 'I_n, provided a proof that the (implicit) argument is distinct from the largest ordinal, of value n. It maps [0..n) ⊂ 'I_n.+1 onto [0..n) ⊂ 'I_n.
  • lift_S is the shift from 'I_n to 'I_n.+1, ie the value is incremented. It maps [0..n) ⊂ 'I_n into [1..n.+1) ⊂ 'I_n.+1.
  • lower_S is the downshift from 'I_n.+1 to 'I_n, ie the value is decremented, provided a proof that the (implicit) argument is distinct from the smallest ordinal, of value 0. It maps [1..n.+1) ⊂ 'I_n.+1 into [0..n) ⊂ 'I_n.
  • cast_f_ord H casts any function of type 'I_[n1] into the same function of type 'I_[n2], provided a proof H : n1 = n2.
  • first_ord n2 is the canonical injection from 'I_n1 to 'I_(n1 + n2). It maps [0..n1) ⊂ 'I_n1 into [0..n1) ⊂ 'I_(n1 + n2).
  • last_ord n1 is the n1-shift from 'I_n2 to 'I_(n1 + n2). It maps [0..n2) ⊂ 'I_n2 into [n1..n1 + n2) ⊂ 'I_(n1 + n2).
  • concat_l_ord H is the canonical projection from 'I_(n1 + n2) onto 'I_n1, provided a proof that the (implicit) argument is smaller than n1. It maps [0..n1) ⊂ 'I_(n1 + n2) onto [0..n1) ⊂ 'I_n1.
  • concat_r_ord H is the n1-downshift from 'I_(n1 + n2) to 'I_n2, provided a proof that the (implicit) argument is not smaller than n1. It maps [n1..n1 + n2) ⊂ 'I_(n1 + n2) into [0..n2) ⊂ 'I_n2.
  • skip_ord i0 injects 'I_n to 'I_n.+1 by skipping i0. It maps [0..n) ⊂ 'I_n into [0..i0^..n.+1) ⊂ 'I_n.+1.
  • insert_ord i0 projects 'I_n.+1 onto 'I_n by skipping i0, provided a proof that the (implicit) argument is distinct from i0. It maps [0..i0^..n.+1) ⊂ 'I_n.+1 onto [0..n) ⊂ 'I_n.
  • skip_f_ord H i0 transforms any function of type 'I_[n.+1] into a function of type 'I_[n] by skipping the input value i0, provided a proof H that the (implicit) function argument is injective.
  • insert_f_ord p i0 transforms any function p : 'I_[n] into a function of type 'I_[n.+1] by inserting the input value i0 associated with itself.
  • extend_f_S transforms any function of type 'I_{n1,n2} into a function of type 'I_{n1.+1,n2.+1} by mapping the (last) input ordinal, of value n1, to the (last) output ordinal, of value n2.
  • skip2_ord H injects 'I_n to 'I_n.+2 by skipping i0 and i1, provided a proof H : i1 i0. It maps [0..n) ⊂ 'I_n into [0..i0^..i1^..n.+2) ⊂ 'I_n.+2.
  • insert2_ord H H0 H1 projecst 'I_n.+2 to 'I_n by skipping i0 and i1, provided a proof H : i1 i0, and proofs H0 and H1 that the (implicit) argument is distinct from i0 and i1. It maps [0..i0^..i1^..n.+2) ⊂ 'I_n.+2 into [0..n) ⊂ 'I_n.
  • move_ord i0 i1 moves i0 right after i1 (it does nothing when i1 = i0). It maps [0..i0..i1..n.+1) ⊂ 'I_n.+1 into [0..i0^..i1 i0..n.+1) ⊂ 'I_n.+1.
  • transp_ord i0 i1 exchanges i0 and i1 (it does nothing when i1 = i0). It maps [0..i0..i1..n) ⊂ 'I_n into [0..i1..i0..n) ⊂ 'I_n.
  • lenPF P is the cardinal of {i ∈ [0..n) | P i} for any predicate P on 'I_n.
  • filterP_ord enumerates the ordinals satisfying the (implicit) predicate argument P : 'I_n Prop. It maps [0..lenPF P) ⊂ 'I_(lenPF P) into {i ∈ [0..n) | P i} ⊂ 'I_n.
  • unfilterP_ord H projects ordinals to their rank in those satisfying the (implicit) predicate argument P : 'I_n Prop, provided a proof H : P i0 for some (implicit) witness argument i0, with default value ord0 when the predicate is not satisfied. It maps 'I_n onto 'I_(lenPF P).

About the API

The statements are mainly plain-Coq compatible (ie use of Prop instead of bool).

Usage

This module may be used through the import of Subsets.Subsets, Subsets.Subsets_wDep, Algebra.Algebra_wDep, Lebesgue.Lebesgue_p_wDep, or Lebesgue.Bochner.Bochner_wDep, where it is exported.

From Requisite Require Import stdlib.
From Coq Require Import EqdepFacts Bool.

From Requisite Require Import ssr_wMC.
From mathcomp Require Import eqtype seq path bigop boolp.

From Numbers Require Import Numbers_wDep.
From Subsets Require Import Subset Function Function_sub.

Notation "''I_' { m , n }" := ('I_m 'I_n)
  (at level 8, m at level 2, n at level 2, format "''I_' { m , n }").
Notation "''I_' [ n ]" := ('I_{n,n})
  (at level 8, n at level 2, format "''I_' [ n ]").
Notation "''I_' { m , n , p }" := ('I_m 'I_{n,p})
  (at level 8, m at level 2, n at level 2, format "''I_' { m , n , p }").

Notation iota := seq.iota (only parsing).

Section Bool_compl.

Lemma P_1 : (P : Prop) b, P reflect P b nat_of_bool b = 1.
Proof. intros P b HP Hb; rewrite (introT Hb); easy. Qed.

Lemma nP_0 : (P : Prop) b, ¬ P reflect P b nat_of_bool b = 0.
Proof. intros P b HP Hb; rewrite (introF Hb); easy. Qed.

Lemma neqP : {T : eqType} {x y : T}, x y x != y.
Proof. intros; apply /eqP; easy. Qed.

Lemma in_asboolP :
   {n} {P : 'I_n Prop} {i}, P i i \in (fun iasbool (P i)).
Proof. move=>> /asboolP H; easy. Qed.

End Bool_compl.

Section Seq_compl1.

Context {T : Type}.
Context {x0 x : T}.
Context {l : seq T}.
Context {i : nat}.

Lemma nth_cons_l : i = 0 nth x0 (x :: l) i = x.
Proof. intros; subst; apply nth0. Qed.

Lemma nth_cons_r : i 0 nth x0 (x :: l) i = nth x0 l (i - 1).
Proof.
intros Hi; rewrite (nth_ncons _ 1); case_eq (i < 1); try easy.
move⇒ /ltP Hi1; contradict Hi; apply lt_1; easy.
Qed.

Lemma nth_rcons_l : i size l nth x0 (rcons l x) i = nth x0 l i.
Proof.
intros Hi; rewrite nth_rcons; case_eq (i < size l); intros Hi1; try easy.
case_eq (i == size l); intros Hi2; try now contradict Hi; apply /eqP.
symmetry; apply nth_default; rewrite leqNgt Hi1; easy.
Qed.

Lemma nth_rcons_r : i = size l nth x0 (rcons l x) i = x.
Proof.
intros Hi; subst; rewrite nth_rcons; case_eq (size l < size l); intros Hl1.
exfalso; rewrite ltnn in Hl1; easy.
case_eq (size l == size l); intros Hl2; try easy.
exfalso; rewrite eq_refl in Hl2; easy.
Qed.

End Seq_compl1.

Section Seq_compl2.

Context {T : eqType}.
Context {x0 x : T}.
Context {l : seq T}.
Context {i : nat}.

Lemma nth_cons_l_rev :
  x \notin l i size l nth x0 (x :: l) i = x i = 0.
Proof.
intros Hx Hi H; destruct l.
apply /eqP; rewrite leqn0 // in Hi.
destruct (le_dec i 0) as [Hi0 | Hi0]; auto with arith.
apply Nat.nle_gt in Hi0; move: Hi0 ⇒ /ltP Hi0.
contradict Hx; apply /negP /negPn.
rewrite -H (nth_ncons _ 1); case_eq (i < 1); intros Hi1.
contradict Hi0; apply /negP; rewrite -ltnNge //.
clear x H; apply mem_nth; rewrite ltn_psubLR //.
Qed.

Lemma nth_cons_l_rev_uniq :
  uniq (x :: l) i size l nth x0 (x :: l) i = x i = 0.
Proof. move=>> /andP [Hx _]; apply nth_cons_l_rev; easy. Qed.

Lemma nth_rcons_r_rev :
  x \notin l i size l nth x0 (rcons l x) i = x i = size l.
Proof.
intros Hx Hi H; destruct (lastP l) as [| s y].
apply /eqP; rewrite leqn0 // in Hi.
destruct (le_dec (size (rcons s y)) i) as [Hi1 | Hi1].
apply Nat.le_antisymm; try easy; apply /leP; easy.
apply Nat.nle_gt in Hi1; move: Hi1 ⇒ /ltP Hi1.
contradict Hx; apply /negP /negPn.
rewrite -H nth_rcons; case_eq (i < size (rcons s y)); intros Hi2.
clear x H; apply mem_nth; easy.
contradict Hi1; apply /negP; apply negbT; easy.
Qed.

Lemma nth_rcons_r_rev_uniq :
  uniq (rcons l x) i size l nth x0 (rcons l x) i = x i = size l.
Proof.
move=>>; rewrite rcons_uniq.
move⇒ /andP [Hx _]; apply nth_rcons_r_rev; easy.
Qed.

End Seq_compl2.

Section Seq_compl3.

Context {T : eqType}.

Lemma injS_seq_equiv :
   {P : pred T} {sT : subType P} {f : T sT},
    injS P f s, all P s { in s &, injective f }.
Proof.
move=>>; split.
intros H s Hs x y Hx Hy; apply H; [move: Hx | move: Hy]; apply /allP; easy.
intros H x y Hx Hy; apply (H [:: x; y]).
simpl; rewrite Hx Hy; easy.
rewrite !in_cons eq_refl; apply orTb.
rewrite !in_cons eq_refl; apply orbT.
Qed.

End Seq_compl3.

Section Ord_compl1.

Lemma I_0_is_empty : ¬ inhabited 'I_0.
Proof. intros [[n Hn]]; easy. Qed.

Definition I_1_is_unit := ord1.

Lemma I_S_is_nonempty : {n}, inhabited 'I_n.+1.
Proof. intros; apply (inhabits ord0). Qed.

Lemma fun_from_I_S_to_I_0_is_empty : n, ¬ inhabited ('I_{n.+1,0}).
Proof.
intros; apply fun_to_empty_is_empty. apply I_S_is_nonempty. apply I_0_is_empty.
Qed.

Definition fun_from_I_0 (E : Type) : 'I_0 E := fun_from_empty I_0_is_empty.

Lemma fun_from_I_0_inj : {E : Type}, injective (fun_from_I_0 E).
Proof. intros; apply fun_from_empty_is_inj, I_0_is_empty. Qed.

Lemma fun_from_I_0_bij : bijective (fun_from_I_0 'I_0).
Proof. apply injF_bij, fun_from_I_0_inj. Qed.

Lemma injF_leq : {n1 n2} {f : 'I_{n1,n2}}, injective f n1 n2.
Proof. exact inj_leq. Qed.

Lemma injF_le :
   {n1 n2} {f : 'I_{n1,n2}}, injective f (n1 n2)%coq_nat.
Proof. move=>> Hf; apply /leP; move: Hf; apply injF_leq. Qed.

Lemma injF_plus_minus_r :
   {n1 n2} {f : 'I_{n1,n2}}, injective f n1 + (n2 - n1) = n2.
Proof. move=>> /injF_leq /leP; apply nat_plus_minus_r. Qed.

Lemma surjF_leq : {n1 n2} {f : 'I_{n1,n2}}, surjective f n2 n1.
Proof. move=>> /surj_has_right_inv [g /can_inj /injF_leq Hg]; easy. Qed.

Lemma surjF_le :
   {n1 n2} {f : 'I_{n1,n2}}, surjective f (n2 n1)%coq_nat.
Proof. move=>> Hf; apply /leP; move: Hf; apply surjF_leq. Qed.

Lemma surjF_plus_minus_r :
   {n1 n2} {f : 'I_{n1,n2}}, surjective f n2 + (n1 - n2) = n1.
Proof. move=>> /surjF_leq /leP; apply nat_plus_minus_r. Qed.

Definition ord1 {n} : 'I_n.+2 := lift ord0 ord0.

Definition ord_pred_max {n} : 'I_n.+2 := Ordinal ltnSSn.

Lemma ord0_correct : {n}, (ord0 : 'I_n.+1) = 0 :> nat.
Proof. easy. Qed.

Lemma ord1_correct : {n}, (ord1 : 'I_n.+2) = 1 :> nat.
Proof. easy. Qed.

Lemma ord_pred_max_correct : {n}, (ord_pred_max : 'I_n.+2) = n :> nat.
Proof. easy. Qed.

Lemma ord_max_correct : {n}, (ord_max : 'I_n.+1) = n :> nat.
Proof. easy. Qed.

Lemma ord0_equiv : {n} (i : 'I_n.+1), i = ord0 nat_of_ord i = 0.
Proof. intros; split; intros; [subst | apply ord_inj]; easy. Qed.

Lemma ord1_equiv : {n} (i : 'I_n.+2), i = ord1 nat_of_ord i = 1.
Proof. intros; split; intros; [subst | apply ord_inj]; easy. Qed.

Lemma ord_pred_max_equiv :
   {n} (i : 'I_n.+2), i = ord_pred_max nat_of_ord i = n.
Proof. intros; split; intros; [subst | apply ord_inj]; easy. Qed.

Lemma ord_max_equiv :
   {n} (i : 'I_n.+1), i = ord_max nat_of_ord i = n.
Proof. intros; split; intros; [subst | apply ord_inj]; easy. Qed.

Lemma ord2_dec : i : 'I_2, {i = ord0} + {i = ord_max}.
Proof.
intros [i Hi]; destruct (ltn_2_dec Hi); [left | right]; apply ord_inj; easy.
Qed.

Lemma ord3_dec : i : 'I_3, {i = ord0} + {i = ord1} + {i = ord_max}.
Proof.
intros [i Hi]; destruct (ltn_3_dec Hi) as [[H | H] | H];
    [left; left | left; right | right]; apply ord_inj; easy.
Qed.

Lemma ord_lt_0_max :
   {n}, ((ord0 : 'I_n.+2) < (ord_max : 'I_n.+2))%coq_nat.
Proof. intros; apply /ltP; easy. Qed.

Lemma ord2_1_max : (ord1 : 'I_2) = (ord_max : 'I_2).
Proof. apply ord_inj; easy. Qed.

Lemma ord2_0_pred_max : (ord0 : 'I_2) = (ord_pred_max : 'I_2).
Proof. apply ord_inj; easy. Qed.

Lemma ord_lt_0_1 : {n}, ((ord0 : 'I_n.+2) < (ord1 : 'I_n.+2))%coq_nat.
Proof. intros; apply /ltP; easy. Qed.

Lemma ord_lt_0_pred_max :
   {n}, ((ord0 : 'I_n.+3) < (ord_pred_max : 'I_n.+3))%coq_nat.
Proof. intros; apply /ltP; easy. Qed.

Lemma ord_lt_1_max :
   {n}, ((ord1 : 'I_n.+3) < (ord_max : 'I_n.+3))%coq_nat.
Proof. intros; apply /ltP; easy. Qed.

Lemma ord3_1_pred_max : (ord1 : 'I_3) = (ord_pred_max : 'I_3).
Proof. apply ord_inj; easy. Qed.

Lemma ord_lt_neq : {n} {i j : 'I_n}, (i < j)%coq_nat i j.
Proof. intros n i j H; contradict H; rewrite H; apply Nat.nlt_ge; easy. Qed.

Lemma ord_lt_neq_sym : {n} {i j : 'I_n}, (i < j)%coq_nat j i.
Proof. intros; apply not_eq_sym; apply ord_lt_neq; easy. Qed.

Lemma ord_0_not_max : {n}, (ord0 : 'I_n.+2) (ord_max : 'I_n.+2).
Proof. intros; apply ord_lt_neq, ord_lt_0_max. Qed.

Lemma ord_max_not_0 : {n}, (ord_max : 'I_n.+2) (ord0 : 'I_n.+2).
Proof. intros; apply not_eq_sym, ord_0_not_max. Qed.

Lemma ord_0_not_1 : {n}, (ord0 : 'I_n.+2) (ord1 : 'I_n.+2).
Proof. intros; apply ord_lt_neq, ord_lt_0_1. Qed.

Lemma ord_1_not_0 : {n}, (ord1 : 'I_n.+2) (ord0 : 'I_n.+2).
Proof. intros; apply not_eq_sym, ord_0_not_1. Qed.

Lemma ord_0_not_pred_max :
   {n}, (ord0 : 'I_n.+3) (ord_pred_max : 'I_n.+3).
Proof. intros; apply ord_lt_neq, ord_lt_0_pred_max. Qed.

Lemma ord_pred_max_not_0 :
   {n}, (ord_pred_max : 'I_n.+3) (ord0 : 'I_n.+3).
Proof. intros; apply not_eq_sym, ord_0_not_pred_max. Qed.

Lemma ord_1_not_max : {n}, (ord1 : 'I_n.+3) (ord_max : 'I_n.+3).
Proof. intros; apply ord_lt_neq, ord_lt_1_max. Qed.

Lemma ord_max_not_1 : {n}, (ord_max : 'I_n.+3) (ord1 : 'I_n.+3).
Proof. intros; apply not_eq_sym, ord_1_not_max. Qed.

Lemma ord2_lt :
   {i0 i1 : 'I_2}, (i0 < i1)%coq_nat i0 = ord0 i1 = ord_max.
Proof.
intros i0 i1; destruct (ord2_dec i0) as [H0 | H0], (ord2_dec i1) as [H1 | H1];
    rewrite H0 H1; try easy.
intros H; contradict H; apply Nat.nlt_ge; easy.
Qed.

Lemma ord3_lt :
   {i0 i1 i2 : 'I_2},
    (i0 < i1)%coq_nat (i1 < i2)%coq_nat
    i0 = ord0 i1 = ord1 i2 = ord_max.
Proof.
intros i0 i1 i2; destruct (ord2_dec i0) as [H0 | H0],
    (ord2_dec i1) as [H1 | H1], (ord2_dec i2) as [H2 | H2];
    rewrite H0 H1 H2; try easy.
intros _ H; contradict H; apply Nat.nlt_ge; easy.
intros H; contradict H; apply Nat.nlt_ge; easy.
Qed.

Lemma ord_compat : {n} {i j : 'I_n}, i = j i = j :> nat.
Proof. intros; subst; easy. Qed.

Lemma ord_neq :
   {n} {i j : 'I_n}, nat_of_ord i nat_of_ord j i j.
Proof. move=>>; apply contra_not, f_equal. Qed.

Lemma ord_neq_compat :
   {n} {i j : 'I_n}, i j nat_of_ord i nat_of_ord j.
Proof. move=>>; apply contra_not, ord_inj. Qed.

Lemma ord_eq_dec : {n} (i j : 'I_n), {i = j} + {i j}.
Proof.
intros n [i Hi] [j Hj]; destruct (Nat.eq_dec i j) as [H | H];
    [left; apply ord_inj | right; apply ord_neq]; easy.
Qed.

Lemma ord_eq2_dec :
   {n} (k i j : 'I_n), {k = i} + {k = j} + {k i k j}.
Proof.
intros n k i j.
destruct (ord_eq_dec k i) as [Hi | Hi]; [left; left; easy |].
destruct (ord_eq_dec k j) as [Hj | Hj]; [left; right | right]; easy.
Qed.

Lemma ord_neq_ex : {n} (i0 : 'I_n.+2), i1, i1 i0.
Proof.
intros n i0; destruct (ord_eq_dec i0 ord0) as [-> | Hi0].
ord_max; apply ord_max_not_0.
ord0; apply not_eq_sym; easy.
Qed.

Lemma ord0_leq_equiv : m {n} {i : 'I_n.+1}, i = ord0 i @ord0 m.
Proof.
intros; rewrite ord0_equiv; destruct i as [i Hi]; simpl.
split; [intros; subst | move⇒ /leP]; auto with arith.
Qed.

Lemma ord0_le_equiv :
   m {n} {i : 'I_n.+1}, i = ord0 (i @ord0 m)%coq_nat.
Proof.
intros m n i; rewrite (ord0_leq_equiv m); split; move⇒ /leP; easy.
Qed.

Lemma ord_n0_gtn_equiv : m {n} {i : 'I_n.+1}, i ord0 @ord0 m < i.
Proof. intros; rewrite -iff_not_r_equiv ord0_leq_equiv nltn_geq; easy. Qed.

Lemma ord_n0_gt_equiv :
   m {n} {i : 'I_n.+1}, i ord0 (@ord0 m < i)%coq_nat.
Proof.
intros m n i; rewrite (ord_n0_gtn_equiv m); split; move⇒ /ltP; easy.
Qed.

Lemma ord_n0_nlt_equiv :
   {n} {i : 'I_n.+1}, i ord0 ¬ (i < 1)%coq_nat.
Proof.
intros; split.
intros H; contradict H; apply ord_inj; simpl; auto with zarith.
rewrite -contra_equiv; intros; subst; apply Nat.lt_0_1.
Qed.

Lemma ord0_lt_equiv : {n} {i : 'I_n.+1}, i = ord0 (i < 1)%coq_nat.
Proof. move=>>; rewrite iff_not_equiv; apply ord_n0_nlt_equiv. Qed.

Lemma ord_n0_gt : {n} {i j : 'I_n.+1}, (i < j)%coq_nat j ord0.
Proof.
intros n i j H; contradict H; rewrite H; apply Nat.nlt_ge; apply /leP; easy.
Qed.

Lemma ord_max_geq_equiv :
   {n} {i : 'I_n.+1}, i = ord_max @ord_max n i.
Proof.
intros; rewrite ord_max_equiv; destruct i as [i Hi]; simpl; split;
    [intros; subst | move⇒ /leP; move: Hi ⇒ /leP]; auto with zarith.
Qed.

Lemma ord_max_ge_equiv :
   {n} {i : 'I_n.+1}, i = ord_max (@ord_max n i)%coq_nat.
Proof. intros; rewrite ord_max_geq_equiv; split; move⇒ /leP; easy. Qed.

Lemma ord_nmax_ltn_equiv :
   {n} {i : 'I_n.+1}, i ord_max i < @ord_max n.
Proof. intros; rewrite -iff_not_r_equiv ord_max_geq_equiv nltn_geq; easy. Qed.

Lemma ord_nmax_lt_equiv :
   {n} {i : 'I_n.+1}, i ord_max (i < @ord_max n)%coq_nat.
Proof. intros; rewrite ord_nmax_ltn_equiv; split; move⇒ /ltP; easy. Qed.

Lemma ord_nmax_lt :
   {n} {i j : 'I_n.+1}, (i < j)%coq_nat i ord_max.
Proof.
intros n i [j Hj] H; apply ord_lt_neq; simpl in ×.
apply nat_lt_lt_S with j; try easy; apply /ltP; easy.
Qed.

Lemma ord_lt_S : {n} (i : 'I_n), i.+1 < n.+1.
Proof.
intros n [i Hi]; apply /ltP; rewrite -Nat.succ_lt_mono; apply /ltP; easy.
Qed.

Lemma ordS_lt_minus_1 :
   {n} (i : 'I_n.+1), nat_of_ord i O i - 1 < n.
Proof.
intros n [i Hi1] Hi2; simpl in *; rewrite ltn_subLR; try easy.
apply /ltP; apply Nat.neq_0_lt_0; easy.
Qed.

Lemma ord_split_gen :
   {n p} (i : 'I_p), (p n.+1)%coq_nat n = i + (n - i).
Proof.
intros n p i Hp; rewrite addn_subn; try easy.
apply Nat.lt_le_trans with p; try apply /ltP; easy.
Qed.

Lemma ordS_split_gen :
   {n p} (i : 'I_p), (p n)%coq_nat n = i.+1 + (n - i.+1).
Proof.
intros n p i Hp; rewrite addn_subn; try easy.
applyNat.succ_lt_mono; apply Nat.lt_le_trans with p; try apply /ltP; easy.
Qed.

Lemma ord_splitS_gen :
   {n p} (i : 'I_p), (p n.+1)%coq_nat n.+1 = i + (n - i).+1.
Proof. move=>> H; rewrite addnS; apply eq_S, ord_split_gen; easy. Qed.

Lemma ordS_splitS_gen :
   {n p} (i : 'I_p), (p n.+1)%coq_nat n.+1 = i.+1 + (n - i).
Proof. move=>>; rewrite addSnnS; apply ord_splitS_gen. Qed.

Lemma ord_split : {n} (i : 'I_n.+1), n = i + (n - i).
Proof. intros; apply ord_split_gen; easy. Qed.

Lemma ordS_split : {n} (i : 'I_n), n = i.+1 + (n - i.+1).
Proof. intros; apply ordS_split_gen; easy. Qed.

Lemma ord_splitS : {n} (i : 'I_n.+1), n.+1 = i + (n - i).+1.
Proof. intros; apply ord_splitS_gen; easy. Qed.

Lemma ordS_splitS : {n} (i : 'I_n.+1), n.+1 = i.+1 + (n - i).
Proof. intros; apply ordS_splitS_gen; easy. Qed.

Lemma ord_split_pred : {n} (i : 'I_n), n = i + (n - i).
Proof. intros; apply ord_split_gen, nat_leS. Qed.

Lemma ord_splitS_pred : {n} (i : 'I_n), n.+1 = i + (n - i).+1.
Proof. intros; apply ord_splitS_gen, nat_leS. Qed.

Lemma ordS_splitS_pred : {n} (i : 'I_n), n.+1 = i.+1 + (n - i).
Proof. intros; apply ordS_splitS_gen, nat_leS. Qed.

Lemma bump_l : i j, (j < i)%coq_nat bump i j = j.
Proof.
intros i j H; unfold bump.
rewrite (nP_0 (i j)); try apply idP; try easy.
move /leP; apply /Nat.nle_gt; easy.
Qed.

Lemma bump_r : i j, (i j)%coq_nat bump i j = j.+1.
Proof.
intros i j H; unfold bump; simpl.
rewrite (P_1 (i j)); try apply idP; try apply /leP; easy.
Qed.

Lemma bump_r_alt : i j, ¬ (j < i)%coq_nat bump i j = j.+1.
Proof. intros; apply bump_r, Nat.nlt_ge; easy. Qed.

Lemma bump_inj : i, injective (bump i).
Proof.
intros i j0 j1;
    destruct (lt_dec j0 i) as [Hj0 | Hj0], (lt_dec j1 i) as [Hj1 | Hj1];
    try rewrite (bump_l _ _ Hj0); try rewrite (bump_r_alt _ _ Hj0);
    try rewrite (bump_l _ _ Hj1); try rewrite (bump_r_alt _ _ Hj1);
    auto with zarith.
Qed.

Lemma bump_eq : h i j, (bump h i == bump h j) = (i == j).
Proof. intros; rewrite (inj_eq (bump_inj h)); easy. Qed.

Lemma bump_neq : h i j, (bump h i != bump h j) = (i != j).
Proof. intros; rewrite bump_eq; easy. Qed.

Lemma bump_incr : h i j, (bump h i < bump h j) = (i < j).
Proof.
intros h i j; rewrite 2!ltn_neqAle (inj_eq (bump_inj h)) leq_bump2; easy.
Qed.

Lemma bump_comm :
   i0 i1 j0 j1 k,
    i0 = bump i1 j0 i1 = bump i0 j1
    bump i1 (bump j0 k) = bump i0 (bump j1 k).
Proof.
intros i0 i1 j0 j1 k Hi0 Hi1.
destruct (le_lt_dec j0 k) as [H0 | H0];
    [rewrite (bump_r _ _ H0) | rewrite (bump_l _ _ H0)];
(destruct (le_lt_dec j1 k) as [H1 | H1];
    [rewrite (bump_r _ _ H1) | rewrite (bump_l _ _ H1)]).
2,4: destruct (le_lt_dec i0 k) as [H2 | H2];
    [rewrite (bump_r _ _ H2) | rewrite (bump_l _ _ H2)].
1,6: destruct (le_lt_dec i0 k.+1) as [H3 | H3];
    [rewrite (bump_r _ _ H3) | rewrite (bump_l _ _ H3)].
3,4,7,8: destruct (le_lt_dec i1 k) as [H4 | H4];
    [rewrite (bump_r _ _ H4) | rewrite (bump_l _ _ H4)].
1,2,11,12: destruct (le_lt_dec i1 k.+1) as [H5 | H5];
    [rewrite (bump_r _ _ H5) | rewrite (bump_l _ _ H5)].
all: try easy.
all: exfalso.
all: destruct (le_lt_dec i1 j0) as [H6 | H6];
    [rewrite (bump_r _ _ H6) in Hi0 | rewrite (bump_l _ _ H6) in Hi0].
all: destruct (le_lt_dec i0 j1) as [H7 | H7];
    [rewrite (bump_r _ _ H7) in Hi1 | rewrite (bump_l _ _ H7) in Hi1].
all: auto with zarith.
Qed.

Lemma lift_l :
   {n} {i : 'I_n.+1} {j : 'I_n}, (j < i)%coq_nat lift i j = j :> nat.
Proof. intros; simpl; apply bump_l; easy. Qed.

Lemma lift_m : {n} (i : 'I_n.+1) (j : 'I_n), i lift i j :> nat.
Proof. intros; apply /eqP; apply neq_bump. Qed.

Lemma lift_r :
   {n} {i : 'I_n.+1} {j : 'I_n},
    (i j)%coq_nat lift i j = j.+1 :> nat.
Proof. intros; simpl; apply bump_r; easy. Qed.

Lemma lift_lt_l :
   {n} (i : 'I_n.+1) (j : 'I_n),
    (lift i j < i)%coq_nat (j < i)%coq_nat.
Proof.
intros n i j H; destruct (le_lt_dec i j) as [Hj | Hj]; try easy.
rewrite (lift_r Hj) in H; contradict Hj; apply Nat.nle_gt; auto with arith.
Qed.

Lemma lift_lt_r :
   {n} (i : 'I_n.+1) (j : 'I_n),
    (i < lift i j)%coq_nat (i j)%coq_nat.
Proof.
intros n i j H; destruct (le_lt_dec i j) as [Hj | Hj]; try easy.
rewrite (lift_l Hj) in H; contradict Hj; apply Nat.nlt_ge; auto with arith.
Qed.

Lemma lift_m1 :
   {n} (i : 'I_n.+1) (j : 'I_n),
    nat_of_ord i O nat_of_ord j = i.-1 lift ord0 j = i.
Proof.
intros n i j H1 H2; apply ord_inj; simpl; unfold bump; simpl.
rewrite H2 -Nat.sub_1_r; auto with zarith arith.
Qed.

Lemma widen_ord_inj : {n p} (H : n p), injective (widen_ord H).
Proof. move=>> /(f_equal (@nat_of_ord _)) H; apply ord_inj; easy. Qed.

End Ord_compl1.

Section Fun_ord1.


Lemma injF_surj : {n} (p : 'I_[n]), injective p surjective p.
Proof. move=>> /injF_bij /bij_surj; easy. Qed.

Lemma surjF_bij : {n} (p : 'I_[n]), surjective p bijective p.
Proof.
move=>> /surj_has_right_inv [g Hg1]; move: (canF_sym Hg1) ⇒ Hg2.
apply (Bijective Hg2 Hg1).
Qed.

Lemma surjF_inj : {n} (p : 'I_[n]), surjective p injective p.
Proof. move=>> /surjF_bij /bij_inj; easy. Qed.

Lemma injF_surj_equiv : {n} (p : 'I_[n]), injective p surjective p.
Proof. intros; split; [apply injF_surj | apply surjF_inj]. Qed.

Lemma bijF_inj_equiv : {n} (p : 'I_[n]), bijective p injective p.
Proof. intros; split; [apply bij_inj | apply injF_bij]. Qed.

Lemma bijF_surj_equiv : {n} (p : 'I_[n]), bijective p surjective p.
Proof. intros; split; [apply bij_surj | apply surjF_bij]. Qed.

Lemma incl_RgF :
   {n} {p : 'I_[n]} (P : 'I_n Prop), injective p incl P (Rg p).
Proof. move=>> Hp i _; rewrite -(f_inv_can_r (injF_bij Hp) i); easy. Qed.

End Fun_ord1.

Section Fun_ord2.


Context {T1 T2 : finType}.

Context {P1 : pred T1}.
Context {P2 : pred T2}.

Variable f : T1 T2.

Definition fun_sub (Hf : funS P1 P2 f) : {x1 | P1 x1} {x2 | P2 x2} :=
  fun y1
    let x1 := proj1_sig y1 in
    let Hx1 := proj2_sig y1 in
    let x2 := f x1 in
    let Hx2 := Hf (f x1) (Im f P1 x1 Hx1) in
    exist _ x2 Hx2.

Lemma bijS_bijF_sub :
   (Hf : bijS P1 P2 f), bijective (fun_sub (bijS_funS Hf)).
Proof.
intros Hf1; apply bij_ex_uniq_equiv; destruct (bijS_ex_uniq Hf1) as [_ Hf2].
intros [x2 Hx2]; destruct (Hf2 x2 Hx2) as [x1 [[Hx1a Hx1b] Hx1c]].
(exist _ x1 Hx1a); split; unfold fun_sub; simpl.
apply eq_exist; easy.
move⇒ [y1 Hy1a] /= Hy1b; apply eq_sig_fst in Hy1b.
apply eq_exist, Hx1c; split; easy.
Qed.

Lemma bijS_eq_card :
  bijS P1 P2 f #|[ pred x1 | P1 x1 ]| = #|[ pred x2 | P2 x2 ]|.
Proof.
move=>> Hf; rewrite -2!card_sig; apply (bij_eq_card (bijS_bijF_sub Hf)).
Qed.

End Fun_ord2.

Section Ord_compl2.

Context {T : Type}.

Variable x0 : T.

Lemma size_ord_enum : {n}, size (ord_enum n) = n.
Proof. intros; rewrite -(size_map val) val_ord_enum; apply size_iota. Qed.

Lemma nth_ord_enum_alt :
   {n} i0 {j} (Hj : j < n), nth i0 (ord_enum n) j = Ordinal Hj.
Proof.
intros n i0 j Hj; apply val_inj; rewrite -(nth_map _ (val i0));
    [rewrite val_ord_enum nth_iota | rewrite size_ord_enum]; easy.
Qed.

Lemma nth_ord_enum : {n} i0 {i : 'I_n}, nth i0 (ord_enum n) i = i.
Proof. intros n i0 [j Hj]; apply nth_ord_enum_alt. Qed.

Lemma map_nth_ord_enum :
   (l : seq T),
    map (fun i : 'I_(size l)nth x0 l i) (ord_enum (size l)) = l.
Proof.
intros l; move: (map_nth_iota0 x0 (leqnn (size l))).
rewrite take_size -val_ord_enum -map_comp; easy.
Qed.

Lemma map_nth_invF :
   {n l1 l2}, size l1 = n.+1 size l2 = n.+1
     {p : 'I_[n.+1]} (Hp : injective p),
      let q := f_inv (injF_bij Hp) in
      l2 = map ((nth x0 l1) \o p) (ord_enum n.+1)
      l1 = map ((nth x0 l2) \o q) (ord_enum n.+1).
Proof.
intros n l1 l2 Hl1 Hl2 p Hp q H.
apply (@eq_from_nth _ x0); [rewrite size_map size_ord_enum; easy |].
intros i Hi; rewrite Hl1 in Hi; pose (ii := Ordinal Hi).
assert (Hii : val ii < size (ord_enum n.+1)) by now rewrite size_ord_enum.
assert (Hq : j : 'I_n.+1, q j < size (ord_enum n.+1))
    by now rewrite size_ord_enum.
rewrite H; unfold comp; replace i with (val ii) by easy.
rewrite !(nth_map ord0)// !nth_ord_enum f_inv_can_r; easy.
Qed.

Definition in_ordS {n} (j : nat) : 'I_n.+1 :=
  match (lt_dec j n.+1) with
  | left HjOrdinal (lt_ltn Hj)
  | right _ord0
  end.

Lemma in_ordS_correct_l : {n} (i : 'I_n.+1), in_ordS i = i.
Proof.
intros n [j Hj]; simpl; unfold in_ordS; destruct (lt_dec _ _) as [Hj' | Hj'].
apply ord_inj; easy.
contradict Hj'; apply /ltP; easy.
Qed.

Lemma in_ordS_correct_l_alt :
   {n} j (Hj : j < n.+1), in_ordS j = Ordinal Hj.
Proof. intros; apply (in_ordS_correct_l (Ordinal _)). Qed.

Lemma in_ordS_correct_r :
   {n} j, ¬ j < n.+1 in_ordS j = (@ord0 n).
Proof.
intros n j Hj; unfold in_ordS; destruct (lt_dec _ _) as [Hj' | Hj']; [| easy].
contradict Hj; apply /ltP; easy.
Qed.

Lemma val_in_ordS : {n} j, j < n.+1 val (@in_ordS n j) = j.
Proof. intros; rewrite in_ordS_correct_l_alt; easy. Qed.

Lemma in_ordS_injS : {n}, injS (fun jj < n.+1) (@in_ordS n).
Proof.
move=>> Hj1 Hj2; rewrite !in_ordS_correct_l_alt.
move⇒ /(f_equal (@nat_of_ord _)); easy.
Qed.

Lemma ord_enumS_eq : {n}, ord_enum n.+1 = map in_ordS (iota 0 n.+1).
Proof.
intros n; apply (@eq_from_nth _ ord0).
rewrite size_ord_enum size_map size_iota; easy.
intros j Hj; rewrite (nth_map 0);
    [| rewrite size_ord_enum in Hj; rewrite size_iota; easy].
rewrite size_ord_enum in Hj; apply sym_eq.
rewrite (nth_iota _ _ Hj) -add0n_sym nth_ord_enum_alt.
apply in_ordS_correct_l_alt.
Qed.

End Ord_compl2.

Section Ord_compl3a.

Context {T : Type}.

Variable leT : rel T.
Variable x0 : T.

Lemma perm_ord_enum_sort :
   l,
    { il | perm_eq il (ord_enum (size l)) uniq il &
      sort leT l = map (fun i : 'I_(size l)nth x0 l i) il }.
Proof.
intros l; pose (n := size l); fold n.
assert (Hl : size l = n) by easy; destruct n as [| n].
([::]); [| apply size0nil; rewrite size_sort]; easy.
destruct (perm_iota_sort leT x0 l) as [jl Hjl2 Hjl1]; rewrite Hl in Hjl2.
pose (il := map in_ordS jl : seq 'I_n.+1); il; [split |].
rewrite ord_enumS_eq; apply perm_map; easy.
rewrite map_inj_in_uniq; [rewrite (perm_uniq Hjl2); apply iota_uniq |].
apply injS_seq_equiv; [apply in_ordS_injS |].
rewrite (perm_all _ Hjl2); apply /allPP; [intros; apply /ltP |].
intros j Hj; rewrite mem_iota in Hj; apply /ltP; easy.
rewrite Hjl1; replace jl with (map val il); [rewrite -map_comp; easy |].
apply (@eq_from_nth _ 0); [rewrite !size_map; easy |].
intros j Hj; rewrite !size_map in Hj.
rewrite -map_comp (nth_map 0)// comp_correct val_in_ordS//.
apply (@proj2 (0 nth 0 jl j)); apply /andP.
rewrite -mem_iota -(perm_mem Hjl2 (nth 0 jl j)); apply mem_nth; easy.
Qed.

End Ord_compl3a.

Section Ord_compl3b.

Context {T : eqType}.
Context {leT : rel T}.

Lemma sorted_ordP :
   {l : seq T} x0 x1,
    reflect ( (i : 'I_(size l)) (Hi1 : i.+1 < size l),
              leT (nth x0 l i) (nth x1 l (Ordinal Hi1)))
            (sorted leT l).
Proof.
intros l x0 x1; apply (iffP (sortedP x0)); intros H.
intros [i Hi] Hi1; simpl; rewrite (set_nth_default x0 x1)//; apply H; easy.
intros i Hi1; rewrite (set_nth_default x1 x0 Hi1).
assert (Hi : i < size l) by now apply ltn_trans with i.+1.
apply (H (Ordinal Hi) Hi1).
Qed.

Hypothesis HT0 : antisymmetric leT.
Hypothesis HT1 : transitive leT.
Hypothesis HT2 : total leT.

Variable x0 : T.

Lemma perm_EX :
   {l1 l2}, perm_eq l1 l2
    { p : 'I_[size l2] | injective p &
      l1 = map ((nth x0 l2) \o p) (ord_enum (size l2)) }.
Proof.
intros l1 l2 Hla.
assert (Hlb : size l1 = size l2) by now apply perm_size.
pose (n := size l2); assert (Hn : size l2 = n) by easy.
fold n in Hlb; fold n; destruct n as [| n].
(fun_from_I_0 'I_0); [apply fun_from_I_0_inj |].
rewrite (size0nil Hlb) (size0nil size_ord_enum); easy.
pose (In := ord_enum n.+1); fold In.
move: (perm_sortP HT2 HT1 HT0 _ _ Hla) ⇒ Hlc.
pose (s := sort leT l2); assert (Hsa : sort leT l1 = s) by easy.
assert (Hsb : size s = n.+1) by now rewrite size_sort.
destruct (perm_ord_enum_sort leT x0 l1) as [il1 [Hil1a Hil1b] Hil1c].
rewrite Hlb in il1, Hil1a, Hil1b, Hil1c; fold In in Hil1a; rewrite Hsa in Hil1c.
assert (Hil1d : size il1 = n.+1) by now rewrite (perm_size Hil1a) size_ord_enum.
pose (p1 := fun i : 'I_n.+1nth ord0 il1 i).
assert (Hp1 : injective p1)
  by now move=>> /eqP H; apply /eqP; move: H; rewrite (nth_uniq ord0)// Hil1d.
pose (q1 := f_inv (injF_bij Hp1) : 'I_[n.+1]).
assert (Hil1e : il1 = map p1 In).
  unfold p1, In; move: (map_nth_ord_enum ord0 il1) ⇒ H.
  rewrite -{1}H Hil1d; easy.
rewrite Hil1e -map_comp in Hil1c.
assert (Hs1 : l1 = map ((nth x0 s) \o q1) In) by now apply map_nth_invF.
destruct (perm_ord_enum_sort leT x0 l2) as [il2 [Hil2a Hil2b] Hil2c].
rewrite Hn in il2, Hil2a, Hil2b, Hil2c; fold In in Hil2a; fold s in Hil2c.
assert (Hil2d : size il2 = n.+1) by now rewrite (perm_size Hil2a) size_ord_enum.
pose (p2 := fun i : 'I_n.+1nth ord0 il2 i).
assert (Hp2 : injective p2)
  by now move=>> /eqP H; apply /eqP; move: H; rewrite (nth_uniq ord0)// Hil2d.
pose (q2 := f_inv (injF_bij Hp2) : 'I_[n.+1]).
assert (Hil2e : il2 = map p2 In).
  unfold p2, In; move: (map_nth_ord_enum ord0 il2) ⇒ H.
  rewrite -{1}H Hil2d; easy.
rewrite Hil2e -map_comp in Hil2c.
assert (Hs2 : l2 = map ((nth x0 s) \o q2) In) by now apply map_nth_invF.
(p2 \o q1); [apply inj_comp_compat; [apply f_inv_inj | easy] |].
rewrite Hs1 Hs2; unfold comp.
apply (@eq_from_nth _ x0); [rewrite !size_map; easy |].
intros i Hi; rewrite size_map size_ord_enum in Hi; pose (ii := Ordinal Hi).
assert (Hii : val ii < size In) by now rewrite size_ord_enum.
replace i with (val ii) by easy.
rewrite !(nth_map ord0)//; [| rewrite size_ord_enum; easy].
rewrite !nth_ord_enum; unfold q2; rewrite f_inv_can_l; easy.
Qed.

Lemma sort_perm_EX :
   l, { p : 'I_[size l] | injective p &
    sort leT l = map (fun inth x0 l (p i)) (ord_enum (size l)) }.
Proof. intros l; apply (perm_EX (permEl (perm_sort leT l))). Qed.

End Ord_compl3b.

Section Ord_compl4a0.

Definition and properties of sortedF/sortedF_S.

Context {T : Type}.

Variable leT : T T Prop.

Definition sortedF {n} (A : 'I_n T) :=
   (i j : 'I_n), (i < j)%coq_nat leT (A i) (A j).

Definition sortedF_S {n} (A : 'I_n T) :=
   (i : 'I_n) (Hi1 : i.+1 < n), leT (A i) (A (Ordinal Hi1)).

Lemma sortedF_nil : (A : 'I_0 T), sortedF A.
Proof. intros A i; destruct i; easy. Qed.

Lemma sortedF_one : (A : 'I_1 T), sortedF A.
Proof. move=>> H; contradict H; rewrite !I_1_is_unit; apply Nat.lt_irrefl. Qed.

Lemma sortedF_inj :
   {n} {A : 'I_n T}, ( x, ¬ leT x x) sortedF A injective A.
Proof.
intros n A HT HA i j H1.
assert (HT' : x y, leT x y x y)
    by now move=>>; rewrite contra_not_r_equiv; intro; subst.
destruct (lt_eq_lt_dec i j) as [[H2 | H2] | H2]; [..| apply sym_eq in H1].
1,3: contradict H1; apply HT', HA; easy.
apply ord_inj; easy.
Qed.

Lemma sortedF_sortedF_S :
   {n} {A : 'I_n T}, sortedF A sortedF_S A.
Proof. move=>> HA i Hi1; apply HA; apply /ltP; apply ltnSn. Qed.

Lemma sortedF_S_sortedF_aux :
   {n} {A : 'I_n T},
    ( x y z, leT x y leT y z leT x z)
    ( p (i : 'I_n) (H : i + p + 1 < n), leT (A i) (A (Ordinal H)))
    sortedF A.
Proof.
intros n A HT HA i j H1.
assert (H2 : i j) by now apply /leP; apply Nat.lt_le_incl.
assert (H3 : i + (j - i - 1) + 1 = j).
  rewrite addnBA; [| rewrite subn_gt0; apply /ltP; easy].
  rewrite subnK; rewrite subnKC//.
  apply leq_ltn_trans with i; [| apply /ltP]; easy.
assert (Hj : (i + (j - i - 1) + 1 < n)) by now rewrite H3.
replace j with (Ordinal Hj); [apply HA | apply ord_inj; easy].
Qed.

Lemma sortedF_S_sortedF :
   {n} {A : 'I_n T},
    ( x y z, leT x y leT y z leT x z)
    sortedF_S A sortedF A.
Proof.
intros n A HT HA; apply (sortedF_S_sortedF_aux HT).
apply (nat_ind_strong (fun p i H, leT (A i) (A (Ordinal H)))).
intros p; destruct p as [|p]; intros Hp i H1.
assert (H2 : i.+1 = i + 0 + 1) by now rewrite -addn0_sym addn1.
assert (H3 : i.+1 < n) by now rewrite H2.
replace (Ordinal _) with (Ordinal H3); [apply HA | apply ord_inj; easy].
assert (H2 : i + p + 1 < n)
    by now apply ltn_trans with (i + p.+1 + 1); [rewrite ltn_add2r ltn_add2l |].
apply HT with (A (Ordinal H2)).
apply Hp; apply /ltP; easy.
assert (H3 : (i + p + 1).+1 = i + p.+1 + 1) by now rewrite -addnA !addn1.
assert (H4 : (i + p + 1).+1 < n) by now rewrite H3.
replace (Ordinal H1) with (Ordinal H4); [apply HA | apply ord_inj; easy].
Qed.

Lemma sortedF_equiv :
   {n} {A : 'I_n T},
    ( x y z, leT x y leT y z leT x z)
    sortedF A sortedF_S A.
Proof.
move=>> HT; split; [apply sortedF_sortedF_S | apply (sortedF_S_sortedF HT)].
Qed.

End Ord_compl4a0.

Section Ord_compl4a1.


Context {T : Type}.

Variable ltT leT : T T Prop.

Lemma sortedF_monot :
   {n} {A : 'I_n T},
    ( x y, ltT x y leT x y)
    sortedF ltT A sortedF leT A.
Proof. move=>> HlT HA i j H; apply HlT, HA; easy. Qed.

End Ord_compl4a1.

Section Ord_compl4b.

Definition and properties of ord_le/ord_lt.

Definition ord_le {n} : 'I_n 'I_n Prop := fun i j ⇒ (i j)%coq_nat.
Definition ord_lt {n} : 'I_n 'I_n Prop := fun i j ⇒ (i < j)%coq_nat.

Lemma ord_le_refl : {n} (i : 'I_n), ord_le i i.
Proof. intros; apply Nat.le_refl. Qed.

Lemma ord_le_antisym :
   {n} (i j : 'I_n), ord_le i j ord_le j i i = j.
Proof. intros; apply ord_inj, Nat.le_antisymm; easy. Qed.

Lemma ord_le_trans :
   {n} (i j k : 'I_n), ord_le i j ord_le j k ord_le i k.
Proof. move=>>; apply Nat.le_trans. Qed.

Lemma ord_le_total : {n} (i j : 'I_n), ord_le i j ord_le j i.
Proof. intros; apply nat_le_total. Qed.

Lemma ord_lt_irrefl : {n} (i : 'I_n), ¬ ord_lt i i.
Proof. intros; apply Nat.lt_irrefl. Qed.

Lemma ord_lt_asym :
   {n} (i j : 'I_n), ord_lt i j ¬ ord_lt j i.
Proof. move=>>; apply Nat.lt_asymm. Qed.

Lemma ord_lt_trans :
   {n} (i j k : 'I_n), ord_lt i j ord_lt j k ord_lt i k.
Proof. move=>>; apply Nat.lt_trans. Qed.

Lemma ord_lt_total_strict :
   {n} (i j : 'I_n), i j ord_lt i j ord_lt j i.
Proof. intros; apply nat_lt_total_strict, ord_neq_compat; easy. Qed.

Definition and properties of ord_leq/ord_ltn.

Definition ord_leq {n} : rel 'I_n := fun i ji j.
Definition ord_ltn {n} : rel 'I_n := fun i ji < j.

Lemma ord_leq_refl : {n}, reflexive (@ord_leq n).
Proof. move=>>; apply leqnn. Qed.

Lemma ord_leq_antisym : {n}, antisymmetric (@ord_leq n).
Proof. move=>> H; apply ord_inj, anti_leq; easy. Qed.

Lemma ord_leq_trans : {n}, transitive (@ord_leq n).
Proof. move=>>; apply leq_trans. Qed.

Lemma ord_leq_total : {n} (i j : 'I_n), ord_leq i j || ord_leq j i.
Proof. intros; apply leq_total. Qed.

Lemma ord_ltn_irrefl : {n}, irreflexive (@ord_ltn n).
Proof. move=>>; apply ltnn. Qed.

Lemma ord_ltn_asym :
   {n} (i j : 'I_n), ord_ltn i j && ord_ltn j i = false.
Proof. move=>>; apply ltn_asym. Qed.

Lemma ord_ltn_trans : {n}, transitive (@ord_ltn n).
Proof. move=>>; apply ltn_trans. Qed.

Lemma ord_ltn_total_strict :
   {n} (i j : 'I_n), i != j = ord_ltn i j || ord_ltn j i.
Proof. move=>>; apply neq_ltn. Qed.

Lemma sorted_enum_ord : {n}, sorted ord_ltn (enum 'I_n).
Proof.
intros [| n]; [rewrite (size0nil (size_enum_ord _)); easy |].
apply /(sortedP ord0); intros i Hi1; rewrite size_enum_ord in Hi1.
unfold ord_ltn; rewrite !nth_enum_ord//; apply ltn_trans with i.+1; easy.
Qed.

Lemma sorted_filter_enum_ord :
   {n} (P : 'I_n Prop),
    sorted ord_ltn (filter (fun iasbool (P i)) (enum 'I_n)).
Proof.
intros; apply sorted_filter; [apply ord_ltn_trans | apply sorted_enum_ord].
Qed.

End Ord_compl4b.

Section Ord_compl4c.

Definition and properties of incrF/incrF_S.

Definition incrF {n1 n2} (f : 'I_{n1,n2}) : Prop := sortedF ord_lt f.
Definition incrF_S {n1 n2} (f : 'I_{n1,n2}) : Prop := sortedF_S ord_lt f.
Definition nondecrF {n1 n2} (f : 'I_{n1,n2}) : Prop := sortedF ord_le f.

Lemma incrF_nil : {n} (f : 'I_{0,n}), incrF f.
Proof. intros; apply sortedF_nil. Qed.

Lemma incrF_one : {n} (f : 'I_{1,n}), incrF f.
Proof. intros; apply sortedF_one. Qed.

Lemma incrF_inj :
   {n1 n2} {f : 'I_{n1,n2}}, incrF f injective f.
Proof. move=>>; apply sortedF_inj, ord_lt_irrefl. Qed.

Lemma incrF_equiv : {n1 n2} (f : 'I_{n1,n2}), incrF f incrF_S f.
Proof. intros; apply sortedF_equiv, ord_lt_trans. Qed.

Lemma incrF_comp :
   {n1 n2 n3} {f : 'I_{n1,n2}} {g : 'I_{n2,n3}},
    incrF f incrF g incrF (g \o f).
Proof. move=>> Hf Hg i1 j1 H1; apply Hg, Hf; easy. Qed.

Lemma incrF_0 :
   {n1 n2} (f : 'I_{n1.+1,n2.+1}) (i2 : 'I_n2.+1),
    incrF f Rg f i2 (f ord0 i2)%coq_nat.
Proof.
intros n1 n2 f i2 Hf [i1 _];
    destruct (ord_eq_dec i1 ord0) as [-> | Hi1]; [easy |].
apply Nat.lt_le_incl, Hf, ord_n0_gt_equiv; easy.
Qed.

Lemma incrF_max :
   {n1 n2} (f : 'I_{n1.+1,n2.+1}) (i2 : 'I_n2.+1),
    incrF f Rg f i2 (i2 f ord_max)%coq_nat.
Proof.
intros n1 n2 f i2 Hf [i1 _];
    destruct (ord_eq_dec i1 ord_max) as [-> | Hi1]; [easy |].
apply Nat.lt_le_incl, Hf, ord_nmax_lt_equiv; easy.
Qed.

Lemma incrF_nondecrF :
   {n1 n2} {f : 'I_{n1,n2}}, incrF f nondecrF f.
Proof. move=>>; apply sortedF_monot; move=>>; apply Nat.lt_le_incl. Qed.

End Ord_compl4c.

Section Cast_ord.


Lemma cast_ord_0_equiv :
   {n m} (H : n = m.+1) (i : 'I_n),
    cast_ord H i = ord0 nat_of_ord i = 0.
Proof.
intros; split; intros Hi.
apply (f_equal (@nat_of_ord _)) in Hi; easy.
apply ord_inj; easy.
Qed.

Lemma cast_ord_n0_equiv :
   {n m} (H : n = m.+1) (i : 'I_n),
    cast_ord H i ord0 nat_of_ord i 0.
Proof. intros; rewrite -iff_not_equiv; apply cast_ord_0_equiv. Qed.

Lemma cast_ord_max_equiv :
   {n m} (H : n = m.+1) (i : 'I_n),
    cast_ord H i = ord_max nat_of_ord i = m.
Proof.
intros; split; intros Hi.
apply (f_equal (@nat_of_ord _)) in Hi; easy.
apply ord_inj; easy.
Qed.

Lemma cast_ord_nmax_equiv :
   {n m} (H : n = m.+1) (i : 'I_n),
    cast_ord H i ord_max nat_of_ord i m.
Proof. intros; rewrite -iff_not_equiv; apply cast_ord_max_equiv. Qed.

Lemma cast_ordS_0 :
   {n m} (H : n.+1 = m.+1) i,
    i = ord0 cast_ord H i = ord0.
Proof. intros; subst; apply ord_inj; easy. Qed.

Lemma cast_ordS_0_rev :
   {n m} (H : n.+1 = m.+1) i,
    cast_ord H i = ord0 i = ord0.
Proof.
moven m H i /(f_equal (cast_ord (sym_eq H))); rewrite cast_ordK;
    intros; subst; apply ord_inj; easy.
Qed.

Lemma cast_ordS_0_equiv :
   {n m} (H : n.+1 = m.+1) (i : 'I_n.+1),
    cast_ord H i = ord0 i = ord0.
Proof. intros; split; [apply cast_ordS_0_rev | apply cast_ordS_0]. Qed.

Lemma cast_ordS_n0 :
   {n m} (H : n.+1 = m.+1) i,
    i ord0 cast_ord H i ord0.
Proof. move=>>; rewrite -contra_equiv; apply cast_ordS_0_rev. Qed.

Lemma cast_ordS_n0_rev :
   {n m} (H : n.+1 = m.+1) i,
    cast_ord H i ord0 i ord0.
Proof. move=>>; rewrite -contra_equiv; apply cast_ordS_0. Qed.

Lemma cast_ordS_n0_equiv :
   {n m} (H : n.+1 = m.+1) (i : 'I_n.+1),
    cast_ord H i ord0 i ord0.
Proof. intros; split; [apply cast_ordS_n0_rev | apply cast_ordS_n0]. Qed.

Lemma cast_ordS_max :
   {n m} (H : n.+1 = m.+1) i,
    i = ord_max cast_ord H i = ord_max.
Proof.
intros n m H i Hi; subst; apply ord_inj; simpl; apply Nat.succ_inj in H; easy.
Qed.

Lemma cast_ordS_max_rev :
   {n m} (H : n.+1 = m.+1) i,
    cast_ord H i = ord_max i = ord_max.
Proof.
moven m H i /(f_equal (cast_ord (sym_eq H))); rewrite cast_ordK;
    intros; subst; apply ord_inj; simpl; apply Nat.succ_inj in H; easy.
Qed.

Lemma cast_ordS_max_equiv :
   {n m} (H : n.+1 = m.+1) (i : 'I_n.+1),
    cast_ord H i = ord_max i = ord_max.
Proof. intros; split; [apply cast_ordS_max_rev | apply cast_ordS_max]. Qed.

Lemma cast_ordS_nmax :
   {n m} (H : n.+1 = m.+1) i,
    i ord_max cast_ord H i ord_max.
Proof. move=>>; rewrite -contra_equiv; apply cast_ordS_max_rev. Qed.

Lemma cast_ordS_nmax_rev :
   {n m} (H : n.+1 = m.+1) i,
    cast_ord H i ord_max i ord_max.
Proof. move=>>; rewrite -contra_equiv; apply cast_ordS_max. Qed.

Lemma cast_ordS_nmax_equiv :
   {n m} (H : n.+1 = m.+1) (i : 'I_n.+1),
    cast_ord H i ord_max i ord_max.
Proof. intros; split; [apply cast_ordS_nmax_rev | apply cast_ordS_nmax]. Qed.

Lemma cast_ord_bij : {n m} (H : n = m), bijective (cast_ord H).
Proof. intros; subst; apply injF_bij, cast_ord_inj. Qed.

Lemma cast_ord_surj : {n m} (H : n = m), surjective (cast_ord H).
Proof. intros; subst; apply injF_surj, cast_ord_inj. Qed.

Lemma cast_ord_val :
   {n m} (H : n = m) (i : 'I_n), i = cast_ord H i :> nat.
Proof. easy. Qed.

Lemma cast_ordP :
   (P : nat Prop) {n m} (H : n = m) (i : 'I_n),
    P i P (cast_ord H i).
Proof. easy. Qed.

Lemma cast_ordb :
   (b : nat bool) {n m} (H : n = m) (i : 'I_n),
    b i = b (cast_ord H i).
Proof. easy. Qed.

Lemma ord_max_alt_equiv :
   {n} (H : 0 < n) (i : 'I_n),
    ¬ (i < n.-1)%coq_nat i = Ordinal (subn1_lt H).
Proof.
intros n Hn1 i; generalize (prednK Hn1); intros Hn2.
rewrite (cast_ordP (fun i¬ (i < _)%coq_nat) (sym_eq Hn2)).
rewrite Nat.nlt_ge -ord_max_ge_equiv ord_max_equiv; simpl; split.
intros Hi; apply ord_inj; simpl; rewrite Hi subn1 //.
move=>> ->; simpl; rewrite subn1 //.
Qed.

Lemma cast_ord0_leq_equiv :
   {m n p} (H0 : 0 < m) (H : n = p.+1) {i : 'I_n},
    cast_ord H i = ord0 i Ordinal H0.
Proof.
intros m n p H0 H i; rewrite (cast_ord_val H) (ord0_leq_equiv m); easy.
Qed.

Lemma cast_ord0_le_equiv :
   {m n p} (H0 : 0 < m) (H : n = p.+1) {i : 'I_n},
    cast_ord H i = ord0 (i Ordinal H0)%coq_nat.
Proof.
intros m n p H0 H i; rewrite (cast_ord0_leq_equiv H0); split; move⇒ /leP; easy.
Qed.

Lemma cast_ord_n0_gtn_equiv :
   {m n p} (H0 : 0 < m) (H : n = p.+1) {i : 'I_n},
    cast_ord H i ord0 Ordinal H0 < i.
Proof.
intros; rewrite -iff_not_r_equiv nltn_geq; apply cast_ord0_leq_equiv.
Qed.

Lemma cast_ord_n0_gt_equiv :
   {m n p} (H0 : 0 < m) (H : n = p.+1) {i : 'I_n},
    cast_ord H i ord0 (Ordinal H0 < i)%coq_nat.
Proof.
intros; rewrite -iff_not_r_equiv Nat.nlt_ge; apply cast_ord0_le_equiv.
Qed.

Lemma cast_ord_max_geq_equiv :
   {n p} (H : n = p.+1) {i : 'I_n},
    cast_ord H i = ord_max Ordinal (ltnSn p) i.
Proof. intros n p H i; rewrite (cast_ord_val H) ord_max_geq_equiv; easy. Qed.

Lemma cast_ord_max_ge_equiv :
   {n p} (H : n = p.+1) {i : 'I_n},
    cast_ord H i = ord_max (Ordinal (ltnSn p) i)%coq_nat.
Proof.
intros n p H i; rewrite cast_ord_max_geq_equiv; split; move⇒ /leP; easy.
Qed.

Lemma cast_ord_nmax_ltn_equiv :
   {n p} (H : n = p.+1) {i : 'I_n},
    cast_ord H i ord_max i < Ordinal (ltnSn p).
Proof.
intros; rewrite -iff_not_r_equiv nltn_geq; apply cast_ord_max_geq_equiv.
Qed.

Lemma cast_ord_nmax_lt_equiv :
   {n p} (H : n = p.+1) {i : 'I_n},
    cast_ord H i ord_max (i < Ordinal (ltnSn p))%coq_nat.
Proof.
intros; rewrite -iff_not_r_equiv Nat.nlt_ge; apply cast_ord_max_ge_equiv.
Qed.

Lemma cast_ord_incrF : {n1 n2} (H : n1 = n2), incrF (cast_ord H).
Proof. easy. Qed.

Lemma incrF_cast_ord_0 :
   {m1 n1 n2} (H1 : m1 = n1.+1) (f : 'I_{m1,n2.+1}) (i2 : 'I_n2.+1),
    incrF f Rg f i2 (f (cast_ord (sym_eq H1) ord0) i2)%coq_nat.
Proof.
intros m1 n1 n2 H1 f i2 Hf [i1 _]; rewrite -(comp_correct _ f).
pose (g := f \o (cast_ord (sym_eq H1))); fold g; apply incrF_0; [| unfold g].
apply incrF_comp; [apply cast_ord_incrF | easy].
apply Rg_ex; (cast_ord H1 i1); rewrite comp_correct cast_ordK; easy.
Qed.

Lemma incrF_cast_ord_max :
   {m1 n1 n2} (H1 : m1 = n1.+1) (f : 'I_{m1,n2.+1}) (i2 : 'I_n2.+1),
    incrF f Rg f i2 (i2 f (cast_ord (sym_eq H1) ord_max))%coq_nat.
Proof.
intros m1 n1 n2 H1 f i2 Hf [i1 _]; rewrite -(comp_correct _ f).
pose (g := f \o (cast_ord (sym_eq H1))); fold g; apply incrF_max; [| unfold g].
apply incrF_comp; [apply cast_ord_incrF | easy].
apply Rg_ex; (cast_ord H1 i1); rewrite comp_correct cast_ordK; easy.
Qed.

Definition and properties of cast_f_ord.

Definition cast_f_ord {n1 n2} (H : n1 = n2) (p1 : 'I_[n1]) : 'I_[n2] :=
  fun i2cast_ord H (p1 (cast_ord (sym_eq H) i2)).

Lemma cast_f_ord_refl :
   {n} (H : n = n) (p : 'I_[n]), cast_f_ord H p = p.
Proof.
intros; apply fun_ext; intro; unfold cast_f_ord; rewrite !cast_ord_id; easy.
Qed.

Lemma cast_f_ord_id :
   {n1 n2} (H : n1 = n2) {p1 : 'I_[n1]},
    same_fun p1 id cast_f_ord H p1 = id.
Proof. move=>>; subst; rewrite cast_f_ord_refl; apply fun_ext. Qed.

Lemma cast_f_ord_inj :
   {n1 n2} (H : n1 = n2) {p1 : 'I_[n1]},
    injective p1 injective (cast_f_ord H p1).
Proof. intros; subst; rewrite cast_f_ord_refl; easy. Qed.

Lemma cast_f_ord_bij :
   {n1 n2} (H : n1 = n2) {p1 : 'I_[n1]},
    injective p1 bijective (cast_f_ord H p1).
Proof. intros; apply injF_bij, cast_f_ord_inj; easy. Qed.

Lemma cast_f_ord_surj :
   {n1 n2} (H : n1 = n2) {p1 : 'I_[n1]},
    injective p1 surjective (cast_f_ord H p1).
Proof. intros; apply injF_surj, cast_f_ord_inj; easy. Qed.

Lemma cast_f_ord_comp :
   {n1 n2} (H : n1 = n2) {p1 q1 : 'I_[n1]},
    cast_f_ord H (p1 \o q1) = (cast_f_ord H p1) \o (cast_f_ord H q1).
Proof. intros; subst; rewrite !cast_f_ord_refl; easy. Qed.

Lemma cast_f_ord_f_inv :
   {n1 n2} (H : n1 = n2) {p1 : 'I_[n1]} (Hp1 : bijective p1),
    cast_f_ord H (f_inv Hp1) = f_inv (cast_f_ord_bij H (bij_inj Hp1)).
Proof.
intros; subst; apply f_inv_uniq_l; intro;
    rewrite !cast_f_ord_refl; apply f_inv_can_l.
Qed.

End Cast_ord.

Section Widen_Lift_S.


Lemma narrow_S_proof : {n} {i : 'I_n.+1}, i ord_max i < n.
Proof.
moven [i Hi1] /ord_neq_compat Hi2; simpl in *; apply ltnSE in Hi1.
apply /ltP; apply Nat.nle_gt; contradict Hi2.
apply Nat.le_antisymm; [apply /leP | ]; easy.
Qed.

Lemma lower_S_proof : {n} {i : 'I_n.+1}, i ord0 i - 1 < n.
Proof.
move=>> Hi; apply ordS_lt_minus_1; contradict Hi; apply ord_inj; easy.
Qed.

Definition widen_S {n} (i : 'I_n) : 'I_n.+1 := widen_ord (leqnSn n) i.

Definition narrow_S {n} {i : 'I_n.+1} (H : i ord_max) : 'I_n :=
  Ordinal (narrow_S_proof H).

Definition lift_S {n} (i : 'I_n) : 'I_n.+1 := lift ord0 i.

Definition lower_S {n} {i : 'I_n.+1} (H : i ord0) : 'I_n :=
  Ordinal (lower_S_proof H).

Lemma widen_S_correct : {n} (i : 'I_n), widen_S i = i :> nat.
Proof. easy. Qed.

Lemma narrow_S_correct :
   {n} {i : 'I_n.+1} (H : i ord_max), narrow_S H = i :> nat.
Proof. easy. Qed.

Lemma lift_S_correct : {n} (i : 'I_n), lift_S i = i.+1 :> nat.
Proof. exact lift0. Qed.

Lemma lower_S_correct :
   {n} {i : 'I_n.+1} (H : i ord0), lower_S H = i.-1 :> nat.
Proof. intros n [i Hi] H; simpl; apply subn1. Qed.

Lemma widen_S_0 : {n}, widen_S (ord0 : 'I_n.+1) = (ord0 : 'I_n.+2).
Proof. intros; apply ord_inj; easy. Qed.

Lemma widen_S_max : {n}, widen_S (ord_max : 'I_n.+1) = (ord_pred_max : 'I_n.+2).
Proof. intros; apply ord_inj; easy. Qed.

Lemma lift_S_0 : {n}, lift_S (ord0 : 'I_n.+1) = (ord1 : 'I_n.+2).
Proof. easy. Qed.

Lemma lift_S_max : {n}, lift_S (ord_max : 'I_n.+1) = (ord_max : 'I_n.+2).
Proof. intros; apply ord_inj; easy. Qed.

Lemma widen_S_not_last : {n} (i : 'I_n), widen_S i ord_max.
Proof. intros; apply ord_lt_neq; simpl; apply /ltP; easy. Qed.

Lemma narrow_widen_S :
   {n} {i : 'I_n} (H : widen_S i ord_max), narrow_S H = i.
Proof. intros; apply ord_inj; easy. Qed.

Lemma widen_narrow_S :
   {n} {i : 'I_n.+1} (H : i ord_max), widen_S (narrow_S H) = i.
Proof. intros; apply ord_inj; easy. Qed.

Lemma lift_S_not_first : {n} (i : 'I_n), (lift_S i) ord0.
Proof. intros; apply not_eq_sym; apply ord_lt_neq; simpl; apply /ltP; easy. Qed.

Lemma lower_lift_S :
   {n} {i : 'I_n} (H : lift_S i ord0), lower_S H = i.
Proof. intros; apply ord_inj; simpl; unfold bump; auto with arith. Qed.

Lemma lower_lift_S_cast_ord :
   {n1 n2} (H12 : n1 = n2) (H21 : n2.+1 = n1.+1)
      {i1 : 'I_n1} (Hi1 : lift_S (cast_ord H12 i1) ord0),
    lower_S (cast_ordS_n0 H21 (lift_S (cast_ord H12 i1)) Hi1) = i1.
Proof. intros; apply ord_inj; simpl; unfold bump; auto with arith. Qed.

Lemma lift_lower_S :
   {n} {i : 'I_n.+1} (H : i ord0), lift_S (lower_S H) = i.
Proof.
intros n i H; apply ord_inj; simpl; apply ord_n0_nlt_equiv, Nat.nlt_ge in H.
rewrite bump_r subn1; auto with zarith.
Qed.

Lemma lift_lower_S_cast_ord :
   {n1 n2} (H12 : n1.+1 = n2.+1) (H21 : n2 = n1)
      {i1 : 'I_n1.+1} (Hi1 : i1 ord0),
    lift_S (cast_ord H21 (lower_S (cast_ordS_n0 H12 _ Hi1))) = i1.
Proof.
moven1 n2 H12 H21 i1 Hi1; apply ord_inj; simpl; rewrite -minusE.
apply ord_n0_nlt_equiv, Nat.nlt_ge in Hi1.
rewritebump_r, subn1; auto with zarith.
Qed.

Lemma lift_widen_S :
   {n} (i : 'I_n), lift_S (widen_S i) = widen_S (lift_S i).
Proof. intros; apply ord_inj; easy. Qed.

Lemma widen_lt_lift_S : {n} (i : 'I_n), (widen_S i < lift_S i)%coq_nat.
Proof. intros; rewrite widen_S_correct lift_S_correct; lia. Qed.

Lemma widen_not_lift_S : {n} (i : 'I_n), widen_S i lift_S i.
Proof. intros; apply ord_lt_neq, widen_lt_lift_S. Qed.

Lemma lift_not_widen_S : {n} (i : 'I_n), lift_S i widen_S i.
Proof. intros; apply not_eq_sym, widen_not_lift_S. Qed.

Lemma widen_S_inj : {n}, injective (@widen_S n).
Proof. intros; apply widen_ord_inj. Qed.

Lemma narrow_S_inj :
   {n},
    injective (fun i : {k : 'I_n.+1 | k ord_max}narrow_S (proj2_sig i)).
Proof.
moven [i Hi] [j Hj] /(f_equal widen_S);
    rewrite !widen_narrow_S; apply eq_exist.
Qed.

Lemma narrow_S_injS :
   {n} {i j : 'I_n.+1} (Hi : i ord_max) (Hj : j ord_max),
    narrow_S Hi = narrow_S Hj i = j.
Proof. move=>> /(f_equal widen_S); rewrite !widen_narrow_S; easy. Qed.

Lemma lift_S_inj : {n}, injective (@lift_S n).
Proof.
intros n; replace (injective lift_S) with (injective (@lift_S n.+1.-1));
    [apply lift_inj | easy].
Qed.

Lemma lower_S_inj :
   {n},
    injective (fun i : {k : 'I_n.+1 | k ord0}lower_S (proj2_sig i)).
Proof.
moven [i Hi] [j Hj] /(f_equal lift_S);
    rewrite !lift_lower_S; apply eq_exist.
Qed.

Lemma lower_S_injS :
   {n} {i j : 'I_n.+1} (Hi : i ord0) (Hj : j ord0),
    lower_S Hi = lower_S Hj i = j.
Proof. move=>> /(f_equal lift_S); rewrite !lift_lower_S; easy. Qed.

Lemma widen_S_incrF : {n}, incrF (@widen_S n).
Proof. easy. Qed.

Lemma narrow_S_incrF :
   {n}, incrF (fun i : 'I_nnarrow_S (widen_S_not_last (widen_S i))).
Proof. move=>>; rewrite !narrow_widen_S; apply widen_S_incrF. Qed.

Lemma narrow_S_incrS :
   {n} {i j : 'I_n.+1} (Hi : i ord_max) (Hj : j ord_max),
    (i < j)%coq_nat (narrow_S Hi < narrow_S Hj)%coq_nat.
Proof. easy. Qed.

Lemma lift_S_incrF : {n}, incrF (@lift_S n).
Proof. move=>> /ltPH; apply /ltP; rewrite bump_incr; easy. Qed.

Lemma lower_S_incrF :
   {n}, incrF (fun i : 'I_nlower_S (lift_S_not_first (lift_S i))).
Proof. move=>>; rewrite !lower_lift_S; apply lift_S_incrF. Qed.

Lemma lower_S_incrS :
   {n} {i j : 'I_n.+1} (Hi : i ord0) (Hj : j ord0),
    (i < j)%coq_nat (lower_S Hi < lower_S Hj)%coq_nat.
Proof.
moven i j Hi Hj /ltP H; apply /ltP; apply ltn_sub2r; [| easy].
apply: (leq_ltn_trans _ H); apply (ord_n0_gtn_equiv n) in Hi; easy.
Qed.

Lemma extF_widenF_S :
   {E : Type} {n} (A B : 'I_n.+1 E),
    (fun iA (widen_S i)) = (fun iB (widen_S i)) A ord_max = B ord_max
    A = B.
Proof.
move=>> /fun_ext_rev H0 H1; apply fun_ext; intros i.
destruct (ord_eq_dec i ord_max) as [-> | Hi];
    [| rewrite -!(widen_narrow_S Hi)]; easy.
Qed.

Lemma extF_liftF_S :
   {E : Type} {n} (A B : 'I_n.+1 E),
    A ord0 = B ord0 (fun iA (lift_S i)) = (fun iB (lift_S i))
    A = B.
Proof.
move=>> H0 /fun_ext_rev H1; apply fun_ext; intros i.
destruct (ord_eq_dec i ord0) as [-> | Hi];
    [| rewrite -!(lift_lower_S Hi)]; easy.
Qed.

End Widen_Lift_S.

Section Ord_compl5.


Lemma Rg_0_liftF_S :
   {n1 n2} {f : 'I_{n1.+1,n2}},
    Rg f = union (eq^~ (f ord0)) (Rg (fun j1f (lift_S j1))).
Proof.
intros n1 n2 f; apply subset_ext_equiv; split.
intros i2 [i1 _]; destruct (ord_eq_dec i1 ord0) as [-> | Hi1]; [left; easy |].
right; rewrite -(lift_lower_S Hi1); apply (Rg_correct (lower_S Hi1)); easy.
intros i2 [-> | [i1 _]]; easy.
Qed.

Lemma incrF_Rg_le_0 :
   {n1 n2} {f g : 'I_{n1.+1,n2}},
    incrF f incrF g Rg f = Rg g (f ord0 g ord0)%coq_nat.
Proof.
intros n1 n2 f g Hf Hg H1;
    destruct (Nat.le_gt_cases (f ord0) (g ord0)) as [H0 | H0]; [easy |].
assert (H2 : Rg f (g ord0)) by now rewrite H1.
induction H2 as [i _]; contradict H0; apply Nat.le_ngt.
destruct (ord_eq_dec i ord0) as [-> | Hi]; [easy |].
apply (incrF_nondecrF Hf), ord_n0_gt_equiv; easy.
Qed.

 Lemma fun_ext_incrF_Rg :
   {n1 n2} {f g : 'I_{n1,n2}},
    incrF f incrF g Rg f = Rg g f = g.
Proof.
intros n1; induction n1; [intros; apply fun_ext; intros [i Hi]; easy |].
intros n2 f g Hf Hg HRg.
assert (H0 : f ord0 = g ord0)
    by now apply ord_inj, Nat.le_antisymm; apply incrF_Rg_le_0.
apply extF_liftF_S; [easy | apply IHn1].
move=>> /ltP H; apply Hf; apply /ltP; easy.
move=>> /ltP H; apply Hg; apply /ltP; easy.
apply union_inj_r with (eq^~ (f ord0)); [| rewrite H0 |].
movei2H1; inversion H1 as [i1 _ Hi1]; apply (incrF_inj Hf) in Hi1; easy.
movei2H1; inversion H1 as [i1 _ Hi1]; apply (incrF_inj Hg) in Hi1; easy.
apply trans_eq with (Rg f); [apply sym_eq | rewrite HRg H0]; apply Rg_0_liftF_S.
Qed.

End Ord_compl5.

Section First_Last_Concat_ord.


Definition first_ord {n1} n2 (i : 'I_n1) : 'I_(n1 + n2) := lshift n2 i.

Definition last_ord n1 {n2} (i : 'I_n2) : 'I_(n1 + n2) := rshift n1 i.

Lemma concat_l_ord_proof :
   {n1 n2} (i : 'I_(n1 + n2)), (i < n1)%coq_nat i < n1.
Proof. move=>> /ltP; easy. Qed.

Lemma concat_r_ord_proof :
   {n1 n2} (i : 'I_(n1 + n2)), ¬ (i < n1)%coq_nat i - n1 < n2.
Proof.
intros; apply /ltP; rewrite <- minusE.
apply nat_lt2_add_lt1_sub_l; try now apply Nat.nlt_ge.
apply /ltP; rewrite plusE; easy.
Qed.

Definition concat_l_ord {n1 n2}
    {i : 'I_(n1 + n2)} (H : (i < n1)%coq_nat) : 'I_n1 :=
  Ordinal (concat_l_ord_proof i H).

Definition concat_r_ord {n1 n2}
    {i : 'I_(n1 + n2)} (H : ¬ (i < n1)%coq_nat) : 'I_n2 :=
  Ordinal (concat_r_ord_proof i H).

Lemma concat_l_first :
   {n1 n2} {i1 : 'I_n1} (H : (first_ord n2 i1 < n1)%coq_nat),
    concat_l_ord H = i1.
Proof. intros; apply ord_inj; easy. Qed.

Lemma first_concat_l :
   {n1 n2} {i : 'I_(n1 + n2)} (H : (i < n1)%coq_nat),
    first_ord n2 (concat_l_ord H) = i.
Proof. intros; apply ord_inj; easy. Qed.

Lemma concat_r_last :
   {n1 n2} {i2 : 'I_n2} (H : ¬ (last_ord n1 i2 < n1)%coq_nat),
    concat_r_ord H = i2.
Proof. intros; apply ord_inj; simpl; auto with arith. Qed.

Lemma last_concat_r :
   {n1 n2} {i : 'I_(n1 + n2)} (H : ¬ (i < n1)%coq_nat),
    last_ord n1 (concat_r_ord H) = i.
Proof. intros; apply ord_inj; simpl; auto with zarith arith. Qed.

End First_Last_Concat_ord.

Section Skip_Insert_ord.


Definition skip_ord {n} (i0 : 'I_n.+1) (j : 'I_n) : 'I_n.+1 :=
  lift i0 (cast_ord (pred_Sn n) j).

Definition insert_ord {n} {i0 i : 'I_n.+1} (H : i i0) : 'I_n :=
  proj1_sig (unlift_some (neqP (not_eq_sym H))).

Lemma insert_ord_inj :
   {n} {i0 i1 i2 : 'I_n.+2} (H1 : i1 i0) (H2 : i2 i0),
    insert_ord H1 = insert_ord H2 i1 = i2.
Proof.
intros n i0 i1 i2 H1 H2 H; unfold insert_ord in H.
destruct (unlift_some (neqP (not_eq_sym H1))) as [j1 Hj1a Hj1b],
    (unlift_some (neqP (not_eq_sym H2))) as [j2 Hj2a Hj2b]; simpl in H.
rewrite Hj2a -H; easy.
Qed.

Lemma insert_ord_neq_compat :
   {n} {i0 i1 i2 : 'I_n.+2} (H1 : i1 i0) (H2 : i2 i0),
    i2 i1 insert_ord H2 insert_ord H1.
Proof. move=>>; apply contra_not, insert_ord_inj. Qed.

Lemma skip_ord_correct_l :
   {n} (i0 : 'I_n.+1) (j : 'I_n),
    (j < i0)%coq_nat skip_ord i0 j = widen_S j.
Proof. intros n i0 j Hj; apply ord_inj; simpl; apply bump_l; easy. Qed.

Lemma skip_ord_correct_m :
   {n} (i0 : 'I_n.+1) (j : 'I_n), skip_ord i0 j i0.
Proof. intros; apply not_eq_sym; apply /eqP; apply neq_lift. Qed.

Lemma skip_ord_correct_r :
   {n} (i0 : 'I_n.+1) (j : 'I_n),
    ¬ (j < i0)%coq_nat skip_ord i0 j = lift_S j.
Proof.
intros; apply ord_inj; simpl.
rewrite !bump_r; [ | apply Nat.le_0_l | apply Nat.nlt_ge]; easy.
Qed.

Lemma skip_ord_0 :
   {n} (i0 : 'I_n.+2), i0 ord0 skip_ord i0 ord0 = ord0.
Proof.
intros n i0 Hi0; rewrite skip_ord_correct_l; try apply widen_S_0.
apply ord_n0_nlt_equiv in Hi0; destruct i0; simpl in *; auto with zarith.
Qed.

Lemma skip_ord_max :
   {n} (i0 : 'I_n.+2), i0 ord_max skip_ord i0 ord_max = ord_max.
Proof.
intros n i0 Hi0; rewrite skip_ord_correct_r; try apply lift_S_max.
apply ord_nmax_lt_equiv in Hi0; destruct i0; simpl in *; auto with zarith.
Qed.

Lemma skip_ord_inj : {n} (i0 : 'I_n.+1), injective (skip_ord i0).
Proof. intros; apply: inj_comp_compat lift_inj; apply cast_ord_inj. Qed.

Lemma insert_ord_compat_P :
   {n} {i0 i : 'I_n.+1} (H H' : i i0), insert_ord H = insert_ord H'.
Proof. intros; f_equal; apply proof_irrel. Qed.

Lemma skip_insert_ord :
   {n} {i0 i : 'I_n.+1} (H : i i0), skip_ord i0 (insert_ord H) = i.
Proof.
intros n i0 i H; unfold skip_ord, insert_ord.
destruct (unlift_some (neqP (not_eq_sym H))) as [j Hj1 Hj2]; simpl.
rewrite Hj1; f_equal; apply ord_inj; easy.
Qed.

Lemma insert_skip_ord :
   {n} {i0 : 'I_n.+1} {j : 'I_n} (H : skip_ord i0 j i0),
    insert_ord H = j.
Proof. intros n i0 j H; apply (skip_ord_inj i0), skip_insert_ord. Qed.

Lemma skip_insert_ord_eq :
   {n} {i0 i : 'I_n.+1} (Hi : i i0) (j : 'I_n),
    skip_ord i0 j = i j = insert_ord Hi.
Proof.
intros n i0 i Hi j; split.
intros Hj; apply (skip_ord_inj i0); rewrite skip_insert_ord; easy.
move⇒ ->; apply skip_insert_ord.
Qed.

Lemma skip_insert_ord_neq :
   {n} {i0 i : 'I_n.+1} (Hi : i i0) (j : 'I_n),
    skip_ord i0 j i j insert_ord Hi.
Proof. intros; rewrite -iff_not_equiv; apply skip_insert_ord_eq. Qed.

Lemma skip_insert_ord_gen :
   {n} (j0 : 'I_n.+1) {j1 j i0 i1}
      (Hj1 : j j1) (Hj2 : skip_ord i0 j i1),
    i0 = skip_ord i1 j0 i1 = skip_ord i0 j1
    skip_ord j0 (insert_ord Hj1) = insert_ord Hj2.
Proof.
intros n j0 j1 j i0 i1 Hj1 Hj2 Hi0 Hi1.
apply skip_insert_ord_eq; unfold skip_ord, insert_ord; simpl.
apply ord_inj; simpl.
destruct (unlift_some (neqP (not_eq_sym Hj1))) as [k Hk1 Hk2]; simpl in ×.
unfold lift in Hk1.
apply (f_equal (@nat_of_ord _)) in Hi0, Hi1, Hk1; simpl in ×.
rewrite Hk1; apply bump_comm; easy.
Qed.

Lemma skip_ord_first : {n} (j : 'I_n), skip_ord ord0 j = lift_S j.
Proof. intros; apply skip_ord_correct_r; easy. Qed.

Lemma skip_ord_last :
   {n} (j : 'I_n), skip_ord ord_max j = widen_S j.
Proof. intros; apply skip_ord_correct_l; apply /ltP; easy. Qed.

Lemma insert_ord_correct_l :
   {n} {i0 i : 'I_n.+1} (H : i i0) (H' : (i < i0)%coq_nat),
    insert_ord H = narrow_S (ord_nmax_lt H').
Proof.
intros n i0 i H H'; apply (skip_ord_inj i0); rewrite skip_insert_ord.
rewrite -{1}(widen_narrow_S (ord_nmax_lt H')).
rewrite skip_ord_correct_l; easy.
Qed.

Lemma insert_ord_correct_r :
   {n} {i0 i : 'I_n.+1} (H : i i0) (H' : (i0 < i)%coq_nat),
    insert_ord H = lower_S (ord_n0_gt H').
Proof.
intros n i0 i H H'; apply (skip_ord_inj i0); rewrite skip_insert_ord.
rewrite -{1}(lift_lower_S (ord_n0_gt H')).
rewrite skip_ord_correct_r; try easy; simpl.
apply Nat.nlt_ge, Nat.lt_succ_r; rewrite subn1 (Nat.lt_succ_pred i0); easy.
Qed.

Lemma insert_ord_monot :
   {n} {i0 i1 i : 'I_n.+2} (H : i1 i0) (H0 : i i0),
    (i < i1)%coq_nat (insert_ord H0 < insert_ord H)%coq_nat.
Proof.
intros n i0 i1 i H H0 H1.
destruct (nat_lt_eq_gt_dec i1 i0) as [[Ha | Ha] | Ha].
2: contradict Ha; apply ord_neq_compat; easy.
assert (H0a : (i < i0)%coq_nat) by auto with zarith.
rewrite 2!insert_ord_correct_l 2!narrow_S_correct; easy.
destruct (nat_lt_eq_gt_dec i i0) as [[H0a | H0a] | H0a].
2: contradict H0a; apply ord_neq_compat; easy.
rewrite insert_ord_correct_l insert_ord_correct_r.
rewrite narrow_S_correct lower_S_correct; auto with zarith.
rewrite 2!insert_ord_correct_r 2!lower_S_correct; auto with zarith.
Qed.

Lemma insert_ord_0 :
   {n} {i0 : 'I_n.+2} (Hi0 : ord0 i0), insert_ord Hi0 = ord0.
Proof. intros; apply sym_eq, skip_insert_ord_eq, skip_ord_0; intuition. Qed.

Lemma insert_ord_max :
   {n} {i0 : 'I_n.+2} (Hi0 : ord_max i0), insert_ord Hi0 = ord_max.
Proof. intros; apply sym_eq, skip_insert_ord_eq, skip_ord_max; intuition. Qed.

Lemma insert_concat_r_ord_0 :
   {n} {i : 'I_n.+1}
      (Hi1 : i ord0) (Hi2 : ¬ (cast_ord (sym_eq (add1n n)) i < 1)%coq_nat),
    insert_ord Hi1 = concat_r_ord Hi2.
Proof.
intros n i Hi1 Hi2; rewrite insert_ord_correct_r.
apply Nat.nle_gt; contradict Hi2; auto with arith.
intros Hi3; apply ord_inj; easy.
Qed.

Lemma insert_concat_l_ord_max :
   {n} {i : 'I_n.+1}
      (Hi1 : i ord_max) (Hi2 : (cast_ord (sym_eq (addn1 n)) i < n)%coq_nat),
    insert_ord Hi1 = concat_l_ord Hi2.
Proof. intros; rewrite insert_ord_correct_l; apply ord_inj; easy. Qed.

Definition and properties of skip_f_ord.

Lemma skip_f_not :
   {n} {p : 'I_[n.+1]} (Hp : injective p) i0 j,
    p (skip_ord i0 j) p i0.
Proof. moven p Hp i0 j /Hp Hj; contradict Hj; apply skip_ord_correct_m. Qed.

Definition skip_f_ord {n} {p : 'I_[n.+1]} (Hp : injective p) i0 : 'I_[n] :=
  fun jinsert_ord (skip_f_not Hp i0 j).

Lemma skip_f_ord_correct :
   {n} {p : 'I_[n.+1]} (Hp : injective p) i0 j,
    skip_ord (p i0) (skip_f_ord Hp i0 j) = p (skip_ord i0 j).
Proof. intros; rewrite skip_insert_ord; easy. Qed.

Lemma skip_f_ord_id :
   {n} {p : 'I_[n.+1]} (Hp : injective p) i0,
    same_fun p id skip_f_ord Hp i0 = id.
Proof.
intros n p Hp1 i0 Hp2; apply fun_ext; intros j.
apply (skip_ord_inj (p i0)); rewrite skip_f_ord_correct !Hp2; easy.
Qed.

Lemma skip_f_ord_inj :
   {n} {p : 'I_[n.+1]} (Hp : injective p) i0,
    injective (skip_f_ord Hp i0).
Proof.
moven p Hp i0 j1 j2 /(f_equal (skip_ord (p i0))) Hj.
rewrite !skip_f_ord_correct in Hj; apply (skip_ord_inj i0), Hp; easy.
Qed.

Lemma skip_f_ord_bij :
   {n} {p : 'I_[n.+1]} (Hp : injective p) i0,
    bijective (skip_f_ord Hp i0).
Proof. intros; apply injF_bij, skip_f_ord_inj. Qed.

Lemma skip_f_ord_surj :
   {n} {p : 'I_[n.+1]} (Hp : injective p) i0,
    surjective (skip_f_ord Hp i0).
Proof. intros; apply injF_surj, skip_f_ord_inj. Qed.

Lemma skip_f_ord_comp :
   {n} {p q : 'I_[n.+1]}
      (Hp : injective p) (Hq : injective q) (H : injective (p \o q)) i0 j,
    skip_f_ord H i0 j = skip_f_ord Hp (q i0) (skip_f_ord Hq i0 j).
Proof.
intros n p q Hp Hq H i0 j; apply (skip_ord_inj (p (q i0))).
rewrite !skip_f_ord_correct; easy.
Qed.

Lemma skip_f_ord_comp_alt :
   {n} {p q : 'I_[n.+1]}
      (Hp : injective p) (Hq : injective q) i0 j,
    skip_f_ord (inj_comp_compat Hq Hp) i0 j =
      skip_f_ord Hp (q i0) (skip_f_ord Hq i0 j).
Proof. intros; apply skip_f_ord_comp. Qed.

Lemma skip_f_ord_f_inv :
   {n} {p : 'I_[n.+1]} (Hp : bijective p) i0,
    skip_f_ord (f_inv_inj Hp) i0 =
      f_inv (skip_f_ord_bij (bij_inj Hp) (f_inv Hp i0)).
Proof.
intros n p Hp i0; apply f_inv_uniq_l; intros j.
rewrite -{1}(f_inv_can_r Hp i0) -skip_f_ord_comp_alt skip_f_ord_id//.
apply f_inv_can_l.
Qed.

Definition and properties of insert_f_ord.

Definition insert_f_ord {n} (p : 'I_[n]) i0 : 'I_[n.+1] :=
  fun imatch (ord_eq_dec i i0) with
    | left _i0
    | right Hskip_ord i0 (p (insert_ord H))
    end.

Lemma insert_f_ord_correct_l :
   {n} (p : 'I_[n]) i0 i, i = i0 insert_f_ord p i0 i = i0.
Proof. intros; unfold insert_f_ord; destruct (ord_eq_dec _ _); easy. Qed.

Lemma insert_f_ord_correct_r :
   {n} (p : 'I_[n]) {i0 i} (H : i i0),
    insert_f_ord p i0 i = skip_ord i0 (p (insert_ord H)).
Proof.
intros; unfold insert_f_ord; destruct (ord_eq_dec _ _);
    [easy | repeat f_equal; apply proof_irrel].
Qed.

Definition and properties of extend_f_S.

Definition extend_f_S {n1 n2} (p : 'I_{n1,n2}) : 'I_{n1.+1,n2.+1} :=
  fun imatch (ord_eq_dec i ord_max) with
    | left _ord_max
    | right Hwiden_S (p (narrow_S H))
    end.

Lemma extend_f_S_correct_l :
   {n1 n2} (p : 'I_{n1,n2}) i, i = ord_max extend_f_S p i = ord_max.
Proof. intros; unfold extend_f_S; destruct (ord_eq_dec _ _); easy. Qed.

Lemma extend_f_S_correct_r :
   {n1 n2} (p : 'I_{n1,n2}) {i} (H : i ord_max),
    extend_f_S p i = widen_S (p (narrow_S H)).
Proof.
intros; unfold extend_f_S; destruct (ord_eq_dec _ _);
    [easy | repeat f_equal; apply proof_irrel].
Qed.

End Skip_Insert_ord.

Section Skip2_Insert2_ord.


Definition skip2_ord
    {n} {i0 i1 : 'I_n.+2} (H : i1 i0) (j : 'I_n) : 'I_n.+2 :=
  skip_ord i0 (skip_ord (insert_ord H) j).

Definition insert2_ord
    {n} {i0 i1 i : 'I_n.+2}
    (H : i1 i0) (H0 : i i0) (H1 : i i1) : 'I_n :=
  insert_ord (insert_ord_neq_compat H H0 H1).

Lemma skip2_ord_compat_P :
   {n} {i0 i1 : 'I_n.+2} (H H' : i1 i0), skip2_ord H = skip2_ord H'.
Proof.
intros; apply fun_ext; intro; unfold skip2_ord; do 2 f_equal.
apply insert_ord_compat_P.
Qed.

Lemma skip2_ord_sym_lt :
   {n} {i0 i1 : 'I_n.+2} (H : (i0 < i1)%coq_nat),
    skip2_ord (ord_lt_neq_sym H) = skip2_ord (ord_lt_neq H).
Proof.
intros n i0 i1 H; apply fun_ext; intros j; apply ord_inj; simpl.
destruct (le_dec (insert_ord (ord_lt_neq_sym H)) j) as [H1 | H1];
    [rewrite (bump_r _ j); try easy | rewrite (bump_l _ j); try now apply Nat.nle_gt];
    rewrite insert_ord_correct_r in H1;
(destruct (le_dec (insert_ord (ord_lt_neq H)) j) as [H2 | H2];
    [rewrite (bump_r (insert_ord _) j); try easy |
     rewrite (bump_l (insert_ord _) j); try now apply Nat.nle_gt];
    rewrite insert_ord_correct_l in H2);
destruct j as [j Hj]; simpl in *; rewrite -minusE in H1.
rewrite (bump_r i0).
rewrite (bump_r i1); auto with zarith.
apply (Nat.le_trans _ j); try apply le_S; easy.
contradict H2; auto with zarith.
rewrite (bump_r i0); try easy.
rewrite (bump_l i1); auto with zarith.
rewrite (bump_l i0); auto with zarith.
rewrite (bump_l i1); auto with zarith.
Qed.

Lemma skip2_ord_sym :
   {n} {i0 i1 : 'I_n.+2} (H10 : i1 i0) (H01 : i0 i1),
    skip2_ord H10 = skip2_ord H01.
Proof.
intros n i0 i1 H10 H01.
destruct (nat_lt_eq_gt_dec i1 i0) as [[Hi | Hi] | Hi].
rewrite (skip2_ord_compat_P _ (ord_lt_neq_sym Hi)) skip2_ord_sym_lt.
apply skip2_ord_compat_P.
contradict H10; apply ord_inj, sym_eq; easy.
rewrite (skip2_ord_compat_P _ (ord_lt_neq_sym Hi)) skip2_ord_sym_lt.
apply skip2_ord_compat_P.
Qed.

Lemma skip2_ord_sym_alt :
   {n} {i0 i1 : 'I_n.+2} (H : i1 i0),
    skip2_ord H = skip2_ord (not_eq_sym H).
Proof. intros; apply skip2_ord_sym. Qed.

Lemma skip2_ord_correct_l :
   {n} {i0 i1 : 'I_n.+2} (H : (i0 < i1)%coq_nat) (j : 'I_n),
    (j < i0)%coq_nat skip2_ord (ord_lt_neq_sym H) j = widen_S (widen_S j).
Proof.
intros n i0 i1 H j Hj; unfold skip2_ord; rewrite skip_ord_correct_l.
f_equal; apply skip_ord_correct_l.
1,2: unfold skip_ord, insert_ord;
    destruct (unlift_some (neqP (not_eq_sym (ord_lt_neq_sym H))))
    as [k Hk1 Hk2]; simpl.
2: rewrite bump_l; try easy.
1,2: apply Nat.lt_le_trans with i0; try easy.
1,2: apply lift_lt_r; rewrite -Hk1; easy.
Qed.

Lemma skip2_ord_correct_m0 :
   {n} {i0 i1 : 'I_n.+2} (H : i1 i0) (j : 'I_n), skip2_ord H j i0.
Proof. intros; apply skip_ord_correct_m. Qed.

Lemma skip2_ord_correct_m :
   {n} {i0 i1 : 'I_n.+2} (H : (i0 < i1)%coq_nat) (j : 'I_n),
    (i0 j)%coq_nat (j < i1.-1)%coq_nat
    skip2_ord (ord_lt_neq_sym H) j = lift_S (widen_S j).
Proof.
intros n i0 i1 H j Hj1 Hj2; unfold skip2_ord; rewrite skip_ord_correct_r.
f_equal; apply skip_ord_correct_l.
1,2: unfold skip_ord, insert_ord;
    destruct (unlift_some (neqP (not_eq_sym (ord_lt_neq_sym H))))
    as [k Hk1 Hk2]; simpl.
2: rewrite bump_l; try now apply Nat.nlt_ge.
1,2: apply Nat.lt_le_trans with i1.-1; try easy.
1,2: apply Nat.eq_le_incl; rewrite Hk1; apply nat_succ_to_pred, lift_r.
1,2: apply lift_lt_r; rewrite -Hk1; easy.
Qed.

Lemma skip2_ord_correct_m1 :
   {n} {i0 i1 : 'I_n.+2} (H : i1 i0) (j : 'I_n), skip2_ord H j i1.
Proof.
intros; rewrite (skip2_ord_sym _ (not_eq_sym _)); apply skip_ord_correct_m.
Qed.

Lemma skip2_ord_correct_r :
   {n} {i0 i1 : 'I_n.+2} (H : (i0 < i1)%coq_nat) (j : 'I_n),
    (i1.-1 j)%coq_nat
    skip2_ord (ord_lt_neq_sym H) j = lift_S (lift_S j).
Proof.
intros n i0 i1 Hi j Hj; unfold skip2_ord; rewrite skip_ord_correct_r.
f_equal; apply skip_ord_correct_r, Nat.nlt_ge.
1,2: unfold skip_ord, insert_ord;
    destruct (unlift_some (neqP (not_eq_sym (ord_lt_neq_sym Hi))))
    as [k Hk1 Hk2]; simpl.
2: rewrite bump_r; auto with zarith.
1,2: apply Nat.le_trans with i1.-1; try easy; rewrite Hk1 lift_r; try easy.
1,2: apply lift_lt_r; rewrite -Hk1; easy.
Qed.

Lemma skip2_ord_inj :
   {n} {i0 i1 : 'I_n.+2} (H : i1 i0), injective (skip2_ord H).
Proof. intros; apply: (inj_comp_compat (skip_ord_inj _)) (skip_ord_inj _). Qed.

Lemma insert_ord2_eq_lt :
   {n} {i0 i1 i : 'I_n.+2}
      (H10 : i1 i0) (H01 : i0 i1) (H0 : i i0) (H1 : i i1)
      (H0' : insert_ord H1 insert_ord H01)
      (H1' : insert_ord H0 insert_ord H10),
    (i0 < i1)%coq_nat insert_ord H0' = insert_ord H1'.
Proof.
intros n i0 i1 i H10 H01 H0 H1 H0' H1' H.
destruct (nat_lt_eq_gt_dec i0 i) as [[H0a | H0a] | H0a].
2: contradict H0a; apply ord_neq_compat, not_eq_sym; easy.
destruct (nat_lt_eq_gt_dec i1 i) as [[H1a | H1a] | H1a].
2: contradict H1a; apply ord_neq_compat, not_eq_sym; easy.
assert (H1b : (insert_ord H10 < insert_ord H0)%coq_nat)
    by now apply insert_ord_monot.
assert (H0b : (insert_ord H01 < insert_ord H1)%coq_nat)
    by now apply insert_ord_monot.
rewrite (insert_ord_correct_r H1') (insert_ord_correct_r H0').
apply ord_inj; rewrite 2!lower_S_correct.
rewrite 2!insert_ord_correct_r; easy.
assert (H1b : (insert_ord H0 < insert_ord H10)%coq_nat)
    by now apply insert_ord_monot.
assert (H0b : (insert_ord H01 < insert_ord H1)%coq_nat)
    by now apply insert_ord_monot.
rewrite (insert_ord_correct_l H1') (insert_ord_correct_r H0').
apply ord_inj; rewrite narrow_S_correct lower_S_correct.
rewrite insert_ord_correct_l insert_ord_correct_r.
rewrite lower_S_correct narrow_S_correct; easy.
assert (H1b : (i < i1)%coq_nat) by now apply Nat.lt_trans with i0.
assert (H1b' : (insert_ord H0 < insert_ord H10)%coq_nat)
    by now apply insert_ord_monot.
assert (H0b : (insert_ord H1 < insert_ord H01)%coq_nat)
    by now apply insert_ord_monot.
rewrite (insert_ord_correct_l H1') (insert_ord_correct_l H0').
apply ord_inj; rewrite 2!narrow_S_correct.
rewrite 2!insert_ord_correct_l; easy.
Qed.

Lemma insert_ord2_eq :
   {n} {i0 i1 i : 'I_n.+2}
      (H10 : i1 i0) (H01 : i0 i1) (H0 : i i0) (H1 : i i1)
      (H0' : insert_ord H1 insert_ord H01)
      (H1' : insert_ord H0 insert_ord H10),
    insert_ord H0' = insert_ord H1'.
Proof.
intros n i0 i1 i H10 H01 H0 H1 H1' H0'.
destruct (nat_lt_eq_gt_dec i1 i0) as [[Ha | Ha] | Ha].
2: contradict Ha; apply ord_neq_compat; easy.
symmetry; apply insert_ord2_eq_lt; easy.
apply insert_ord2_eq_lt; easy.
Qed.

Lemma insert_ord2_eq_alt :
   {n} {i0 i1 i : 'I_n.+2} (H : i1 i0) (H0 : i i0) (H1 : i i1)
      (H0' : insert_ord H1 insert_ord (not_eq_sym H))
      (H1' : insert_ord H0 insert_ord H),
    insert_ord H0' = insert_ord H1'.
Proof. intros; apply insert_ord2_eq. Qed.

Lemma insert2_ord_eq :
   {n} {i0 i1 i : 'I_n.+2} (H : i1 i0) (H0 : i i0) (H1 : i i1)
      (H1' : insert_ord H0 insert_ord H),
    insert2_ord H H0 H1 = insert_ord H1'.
Proof. intros; apply insert_ord_compat_P. Qed.

Lemma insert2_ord_compat_P :
   {n} {i0 i1 i : 'I_n.+2}
      (H H' : i1 i0) (H0 H0' : i i0) (H1 H1' : i i1),
    insert2_ord H H0 H1 = insert2_ord H' H0' H1'.
Proof. intros; f_equal; apply proof_irrel. Qed.

Lemma insert2_ord_sym :
   {n} {i0 i1 i : 'I_n.+2}
      (H10 : i1 i0) (H01 : i0 i1) (H0 : i i0) (H1 : i i1),
    insert2_ord H10 H0 H1 = insert2_ord H01 H1 H0.
Proof. intros; apply insert_ord2_eq. Qed.

Lemma insert2_ord_sym_alt :
   {n} {i0 i1 i : 'I_n.+2} (H : i1 i0) (H0 : i i0) (H1 : i i1),
    insert2_ord H H0 H1 = insert2_ord (not_eq_sym H) H1 H0.
Proof. intros; apply insert2_ord_sym. Qed.

Lemma insert2_ord_eq_sym :
   {n} {i0 i1 i : 'I_n.+2} (H10 : i1 i0) (H01 : i0 i1)
      (H0 : i i0) (H1 : i i1) (H0' : insert_ord H1 insert_ord H01),
    insert2_ord H10 H0 H1 = insert_ord H0'.
Proof. intros; rewrite insert2_ord_sym; apply insert_ord_compat_P. Qed.

Lemma insert2_ord_eq_sym_alt :
   {n} {i0 i1 i : 'I_n.+2} (H : i1 i0) (H0 : i i0) (H1 : i i1)
      (H0' : insert_ord H1 insert_ord (not_eq_sym H)),
    insert2_ord H H0 H1 = insert_ord H0'.
Proof. intros; apply insert2_ord_eq_sym. Qed.

Lemma skip2_insert2_ord :
   {n} {i0 i1 i : 'I_n.+2} (H : i1 i0) (H0 : i i0) (H1 : i i1),
    skip2_ord H (insert2_ord H H0 H1) = i.
Proof. intros; unfold skip2_ord; rewrite 2!skip_insert_ord; easy. Qed.

Lemma insert2_skip2_ord :
   {n} {i0 i1 : 'I_n.+2} {j : 'I_n}
      (H : i1 i0) (H0 : skip2_ord H j i0) (H1 : skip2_ord H j i1),
    insert2_ord H H0 H1 = j.
Proof.
intros n i0 i1 j H H0 H1; apply (skip2_ord_inj H), skip2_insert2_ord.
Qed.

End Skip2_Insert2_ord.

Section Rev_ord.


Lemma rev_ord_correct : {n} (i : 'I_n), rev_ord i = n - i.+1 :> nat.
Proof. easy. Qed.

Lemma rev_ord_0 : {n}, rev_ord (@ord0 n) = ord_max.
Proof. intros; apply ord_inj; simpl; rewrite subn1; easy. Qed.

Lemma rev_ord_r :
   {n} (i : 'I_n), rev_ord (lift_S i) = widen_S (rev_ord i).
Proof. intros; apply ord_inj; simpl; rewrite bump_r; auto with zarith. Qed.

Lemma rev_ord_l :
   {n} (i : 'I_n), rev_ord (widen_S i) = lift_S (rev_ord i).
Proof.
intros; apply ord_inj; simpl; rewrite bump_r; auto with zarith.
rewrite subSS subnSK; easy.
Qed.

Lemma rev_ord_bij : {n}, bijective (@rev_ord n).
Proof. intros; apply injF_bij, rev_ord_inj. Qed.

Lemma rev_ord_surj : {n}, surjective (@rev_ord n).
Proof. intros; apply injF_surj, rev_ord_inj. Qed.

Lemma rev_ord_max : {n}, rev_ord (@ord_max n) = ord0.
Proof. intros; apply ord_inj; simpl; apply subnn. Qed.

Lemma cast_f_rev_ord :
   {n1 n2} (H : n1 = n2), cast_f_ord H (@rev_ord n1) = @rev_ord n2.
Proof. intros; subst; apply fun_ext; intro; apply ord_inj; easy. Qed.

End Rev_ord.

Section Move_ord.

Definition and properties of move_ord.

Definition move_ord {n} (i0 i1 i : 'I_n.+1) : 'I_n.+1 :=
  match (ord_eq_dec i i1) with
  | left _i0
  | right Hskip_ord i0 (insert_ord H)
  end.

Lemma move_ord_correct_l :
   {n} {i0 i1 i : 'I_n.+1}, i = i1 move_ord i0 i1 i = i0.
Proof. intros; unfold move_ord; destruct (ord_eq_dec _ _); easy. Qed.

Lemma move_ord_correct_r :
   {n} (i0 : 'I_n.+1) {i1 i} (Hi : i i1),
    move_ord i0 i1 i = skip_ord i0 (insert_ord Hi).
Proof.
intros; unfold move_ord; destruct (ord_eq_dec _ _); try easy; f_equal.
apply insert_ord_compat_P.
Qed.

Lemma move_ord_inj : {n} (i0 i1 : 'I_n.+1), injective (move_ord i0 i1).
Proof.
intros n i0 i1 i i'; unfold move_ord; destruct (ord_eq_dec _ _) as [Hi | Hi],
    (ord_eq_dec _ _) as [Hi' | Hi']; try now rewrite Hi Hi'.
intros H; contradict H; apply not_eq_sym, skip_ord_correct_m.
intros H; contradict H; apply skip_ord_correct_m.
destruct n as [| n]; [exfalso; rewrite !I_1_is_unit in Hi; easy |].
move⇒ /skip_ord_inj /insert_ord_inj; easy.
Qed.

Lemma move_ord_bij : {n} (i0 i1 : 'I_n.+1), bijective (move_ord i0 i1).
Proof. intros; apply injF_bij, move_ord_inj. Qed.

Lemma move_ord_surj : {n} (i0 i1 : 'I_n.+1), surjective (move_ord i0 i1).
Proof. intros; apply injF_surj, move_ord_inj. Qed.

Lemma move_ord_orth :
   {n} (i0 i1 : 'I_n.+1), cancel (move_ord i0 i1) (move_ord i1 i0).
Proof.
intros n i0 i1 i; destruct (ord_eq_dec (move_ord i0 i1 i) i0) as [Hi0 | Hi0].
rewrite Hi0 move_ord_correct_l//;
    apply (move_ord_inj i0 i1); rewrite move_ord_correct_l; easy.
rewrite (move_ord_correct_r i1).
unfold skip_ord, insert_ord at 1;
    destruct (unlift_some (neqP (not_eq_sym Hi0))) as [j0 Hj0a Hj0b]; simpl in ×.
apply ord_inj; simpl; unfold move_ord in Hj0a;
    destruct (ord_eq_dec i i1) as [Hi1 | Hi1].
contradict Hi0; rewrite Hi1 move_ord_correct_l; easy.
unfold skip_ord, insert_ord, lift in Hj0a;
    destruct (unlift_some (neqP (not_eq_sym Hi1))) as [j1 Hj1a Hj1b]; simpl in ×.
unfold lift in Hj1a; destruct i1 as [i1 H1], i as [i Hi],
    j0 as [j0 Hj0], j1 as [j1 Hj1]; simpl in ×.
apply (f_equal (@nat_of_ord n.+1)) in Hj1a, Hj0a; simpl in ×.
rewrite Hj1a; f_equal; apply (bump_inj i0); easy.
Qed.

Lemma cast_f_move_ord :
   {n1 n2} (H : n1.+1 = n2.+1) (i0 i1 : 'I_n1.+1),
    cast_f_ord H (move_ord i0 i1) = move_ord (cast_ord H i0) (cast_ord H i1).
Proof.
intros n1 n2 H i0 i1; assert (H' : n1 = n2) by lia. subst.
apply fun_ext; intro; unfold cast_f_ord; rewrite !cast_ord_id; easy.
Qed.

End Move_ord.

Section Transp_ord.

Definition and properties of transp_ord.

Definition transp_ord {n} (i0 i1 i : 'I_n) : 'I_n :=
  if ord_eq_dec i i0 then i1 else if ord_eq_dec i i1 then i0 else i.

Lemma transp_ord_sym :
   {n} {i0 i1 : 'I_n}, transp_ord i0 i1 = transp_ord i1 i0.
Proof.
intros n i0 i1; apply fun_ext; intros i; unfold transp_ord.
destruct (ord_eq_dec i i0) as [Hi0 | Hi0],
    (ord_eq_dec i i1) as [Hi1 | Hi1]; simpl; try easy.
rewrite -Hi0; easy.
Qed.

Lemma transp_ord_correct_l0 :
   {n} {i0 i1 i : 'I_n}, i = i0 transp_ord i0 i1 i = i1.
Proof. intros; unfold transp_ord; destruct (ord_eq_dec _ _); easy. Qed.

Lemma transp_ord_correct_l1 :
   {n} {i0 i1 i : 'I_n}, i = i1 transp_ord i0 i1 i = i0.
Proof. move=>>; rewrite transp_ord_sym; apply transp_ord_correct_l0. Qed.

Lemma transp_ord_correct_r :
   {n} {i0 i1 i : 'I_n}, i i0 i i1 transp_ord i0 i1 i = i.
Proof.
intros; unfold transp_ord; destruct (ord_eq_dec _ _), (ord_eq_dec _ _); easy.
Qed.

Lemma transp_ord_inj : {n} (i0 i1 : 'I_n), injective (transp_ord i0 i1).
Proof.
intros n i0 i1 i i'.
destruct (ord_eq2_dec i i0 i1) as [[Hi | Hi] | [Hi1 Hi2]];
    [rewrite (transp_ord_correct_l0 Hi) | rewrite (transp_ord_correct_l1 Hi) |
     rewrite (transp_ord_correct_r Hi1 Hi2)];
(destruct (ord_eq2_dec i' i0 i1) as [[Hi' | Hi'] | [Hi'1 Hi'2]];
    [rewrite (transp_ord_correct_l0 Hi') | rewrite (transp_ord_correct_l1 Hi') |
     rewrite (transp_ord_correct_r Hi'1 Hi'2)]);
    try rewrite Hi; try rewrite Hi'; try easy; intros H; subst; easy.
Qed.

Lemma transp_ord_bij : {n} (i0 i1 : 'I_n), bijective (transp_ord i0 i1).
Proof. intros; apply injF_bij, transp_ord_inj. Qed.

Lemma transp_ord_surj : {n} (i0 i1 : 'I_n), surjective (transp_ord i0 i1).
Proof. intros; apply injF_surj, transp_ord_inj. Qed.

Lemma transp_ord_orth :
   {n} (i0 i1 : 'I_n), cancel (transp_ord i0 i1) (transp_ord i1 i0).
Proof.
intros n i0 i1 i; destruct (ord_eq2_dec i i0 i1) as [[H | H] | [H1 H2]].
rewrite !transp_ord_correct_l0//.
rewrite !transp_ord_correct_l1//.
rewrite !transp_ord_correct_r//.
Qed.

Lemma transp_ord_invol :
   {n} (i0 i1 : 'I_n), involutive (transp_ord i0 i1).
Proof. move=>>; rewrite {1}transp_ord_sym; apply transp_ord_orth. Qed.

Lemma cast_f_transp_ord :
   {n1 n2} (H : n1 = n2) (i0 i1 : 'I_n1),
    cast_f_ord H (transp_ord i0 i1) = transp_ord (cast_ord H i0) (cast_ord H i1).
Proof.
intros; subst; apply fun_ext; intro; unfold cast_f_ord;
    rewrite !cast_ord_id; easy.
Qed.

End Transp_ord.

Section FilterP_ord.


Definition lenPF {n} (P : 'I_n Prop) : nat := #|fun iasbool (P i)|.
Definition filterP_ord
    {n} {P : 'I_n Prop} (j : 'I_(lenPF P)) : 'I_n := enum_val j.
Definition unfilterP_ord
    {n} {P : 'I_n Prop} {i0} (HP0 : P i0) (i : 'I_n) : 'I_(lenPF P) :=
  enum_rank_in (in_asboolP HP0) i.

Lemma lenPF_ext_gen :
   {n1 n2} (H : n1 = n2) {P1 : 'I_n1 Prop} {P2 : 'I_n2 Prop},
    ( i1, P1 i1 P2 (cast_ord H i1)) lenPF P1 = lenPF P2.
Proof.
move=>> H; subst; apply eq_card; intro; apply asbool_equiv_eq.
rewrite H cast_ord_id; easy.
Qed.

Lemma lenPF_ext :
   {n} {P Q : 'I_n Prop},
    ( i, P i Q i) lenPF P = lenPF Q.
Proof.
intros; apply (lenPF_ext_gen (erefl n)); intros; rewrite cast_ord_id //.
Qed.

Lemma lenPF_extb :
   {n} {P : 'I_n Prop} (b : 'I_n bool),
    ( i, P i is_true (b i)) lenPF P = #|b|.
Proof.
move=>> /lenPF_ext ->; unfold lenPF; do 2 f_equal.
apply fun_ext; intro; apply asboolb.
Qed.

Lemma lenPF_le : {n} (P : 'I_n Prop), lenPF P n.
Proof.
intros n P; apply /leP; replace n with (#|'I_n|) by apply card_ord; apply /leP.
apply max_card.
Qed.

Lemma lenPF_nil : (P : 'I_0 Prop), lenPF P = 0.
Proof.
intros; apply eq_card0; apply /pred0P; apply negbNE; apply /pred0Pn.
intros [[i Hi1] Hi2]; easy.
Qed.

Lemma lenPF_nil_alt : {n} (P : 'I_n Prop), n = 0 lenPF P = 0.
Proof. intros; subst; apply lenPF_nil. Qed.

Lemma lenPF0_alt :
   {n} (P : 'I_n Prop), ( i, ¬ P i) lenPF P = 0.
Proof.
intros n P HP; rewrite (lenPF_extb (fun false)); try apply card0.
intros; rewrite falseE; split; [apply HP | easy].
Qed.

Lemma lenPF0 : {n}, lenPF (fun _ : 'I_nFalse) = 0.
Proof. intros; apply lenPF0_alt; easy. Qed.

Lemma lenPF0_rev :
   {n} (P : 'I_n Prop), lenPF P = 0 i, ¬ P i.
Proof.
move=>> /card0_eq HP i /asboolP Hi; apply (eq_true_false_abs _ Hi (HP i)).
Qed.

Lemma lenPF0_equiv :
   {n} (P : 'I_n Prop), lenPF P = 0 i, ¬ P i.
Proof. intros; split; [apply lenPF0_rev | apply lenPF0_alt]. Qed.

Lemma lenPF_n0 :
   {n} {P : 'I_n Prop}, 0 < lenPF P i0, P i0.
Proof.
move=>>; rewrite contra_equiv not_ex_all_not_equiv; intros.
apply /negP; rewrite -eqn0Ngt; apply /eqP; apply lenPF0_alt; easy.
Qed.

Lemma lenPF_n0_rev : {n} {P : 'I_n Prop} {i0}, P i0 0 < lenPF P.
Proof.
move=>>; rewrite -nleq_gtn contra_not_r_equiv leqn0.
move⇒ /eqP HP; apply lenPF0_rev; easy.
Qed.

Lemma lenPF_n0_equiv :
   {n} {P : 'I_n Prop}, 0 < lenPF P i0, P i0.
Proof.
intros; split; [apply lenPF_n0 | intros [i0 HP]; apply (lenPF_n0_rev HP)].
Qed.

Lemma lenPF_n0_alt :
   {n} {P : 'I_n Prop} (j : 'I_(lenPF P)), i0, P i0.
Proof.
intros n P j; apply lenPF_n0; destruct (le_lt_dec (lenPF P) 0) as [HP | HP].
rewrite Nat.le_0_r in HP; rewrite HP in j; destruct j; easy.
apply /ltP; easy.
Qed.

Lemma lenPFS :
   {n} {P : 'I_n Prop} i0, P i0 lenPF P = (lenPF P).-1.+1.
Proof. move=>> HP0; rewrite prednK; [easy | apply (lenPF_n0_rev HP0)]. Qed.

Lemma lenPFmax_alt :
   {n} (P : 'I_n Prop), ( i, P i) lenPF P = n.
Proof.
intros n P HP; rewrite (lenPF_extb (fun true)); [apply card_ord | easy].
Qed.

Lemma lenPFmax : {n}, lenPF (fun _ : 'I_nTrue) = n.
Proof. intros; apply lenPFmax_alt; easy. Qed.

Lemma lenPF_nmax :
   {n} {P : 'I_n Prop}, lenPF P < n i0, ¬ P i0.
Proof.
move=>>; rewrite contra_equiv not_ex_not_all_equiv; intros.
apply /negP; rewrite -leqNgt; apply eq_leq, sym_eq, lenPFmax_alt; easy.
Qed.

Lemma lenPF1_in : {P : 'I_1 Prop}, P ord0 lenPF P = 1.
Proof.
intros; erewrite lenPF_ext; [apply lenPFmax | intros; rewrite I_1_is_unit; easy].
Qed.

Lemma lenPF1_out : {P : 'I_1 Prop}, ¬ P ord0 lenPF P = 0.
Proof.
intros; erewrite lenPF_ext; [apply lenPF0 | intros; rewrite I_1_is_unit; easy].
Qed.

Lemma lenPF_cast_ord :
   {n1 n2} (H : n1 = n2) (P1 : 'I_n1 Prop),
    lenPF P1 = lenPF (fun i2P1 (cast_ord (sym_eq H) i2)).
Proof.
intros; apply: lenPF_ext_gen; intros; rewrite cast_ord_comp cast_ord_id //.
Qed.

Lemma lenPF_ind_l_in :
   {n} {P : 'I_n.+1 Prop},
    P ord0 lenPF P = 1 + lenPF (fun iP (lift_S i)).
Proof.
intros [| n] P; [intros HP; rewrite (lenPF1_in HP) lenPF_nil addn0; easy |].
move⇒ /asboolP HP; unfold lenPF; rewrite (cardD1x HP); f_equal.
apply sym_eq, (bijS_eq_card lift_S), (injS_surjS_bijS I_S_is_nonempty).
apply funS_correct; intro; destruct (pselect _); [| easy].
intros _; apply /andP; split;
    [apply /asboolP; easy | apply neqP, lift_S_not_first].
move=>> _ _; apply: lift_inj.
intros i; destruct (ord_eq_dec i ord0) as [-> | Hi]; move⇒ /andP.
move⇒ [_ /negP Hi]; contradict Hi; easy.
move⇒ [HP' _]; (lower_S Hi); rewrite lift_lower_S; easy.
Qed.

Lemma lenPF_ind_l_in_S :
   {n} {P : 'I_n.+1 Prop},
    P ord0 lenPF P = (lenPF (fun iP (lift_S i))).+1.
Proof. move=>> HP0; rewrite (lenPF_ind_l_in HP0); apply add1n. Qed.

Lemma lenPF_ind_l_out :
   {n} {P : 'I_n.+1 Prop},
    ¬ P ord0 lenPF P = lenPF (fun iP (lift_S i)).
Proof.
intros [| n] P HP; [rewrite (lenPF1_out HP) lenPF_nil; easy |].
apply sym_eq, (bijS_eq_card lift_S), (injS_surjS_bijS I_S_is_nonempty);
    [apply funS_correct; easy | move=>> _ _; apply: lift_inj |].
intros i; destruct (ord_eq_dec i ord0) as [-> | Hi].
rewrite ifF; [| destruct (pselect _)]; easy.
intros; (lower_S Hi); rewrite lift_lower_S; easy.
Qed.

Lemma lenPF_ind_r_in :
   {n} {P : 'I_n.+1 Prop},
    P ord_max lenPF P = lenPF (fun iP (widen_S i)) + 1.
Proof.
intros [| n] P; [rewrite I_1_is_unit; intros HP;
    rewrite (lenPF1_in HP) lenPF_nil add0n; easy |].
move⇒ /asboolP HP; unfold lenPF; rewrite (cardD1x HP) addnC; f_equal.
apply sym_eq, (bijS_eq_card widen_S), (injS_surjS_bijS I_S_is_nonempty).
apply funS_correct; intro; destruct (pselect _); [| easy].
intros _; apply /andP; split;
    [apply /asboolP; easy | apply neqP, widen_S_not_last].
move=>> _ _; apply: widen_ord_inj.
intros i; destruct (ord_eq_dec i ord_max) as [-> | Hi]; move⇒ /andP.
move⇒ [_ /negP Hi]; contradict Hi; easy.
move⇒ [HP' _]; (narrow_S Hi); rewrite widen_narrow_S; easy.
Qed.

Lemma lenPF_ind_r_in_S :
   {n} {P : 'I_n.+1 Prop},
    P ord_max lenPF P = (lenPF (fun iP (widen_S i))).+1.
Proof. move=>> HP; rewrite (lenPF_ind_r_in HP); apply addn1. Qed.

Lemma lenPF_ind_r_in_S_alt :
   {n} {P : 'I_n.+1 Prop},
    P ord_max lenPF (fun iP (widen_S i)) < lenPF P.
Proof. intros; rewrite lenPF_ind_r_in_S; easy. Qed.

Lemma lenPF_ind_r_out :
   {n} {P : 'I_n.+1 Prop},
    ¬ P ord_max lenPF P = lenPF (fun iP (widen_S i)).
Proof.
intros [| n] P HP; [rewrite I_1_is_unit in HP;
    rewrite (lenPF1_out HP) lenPF_nil; easy |].
apply sym_eq, (bijS_eq_card widen_S), (injS_surjS_bijS I_S_is_nonempty);
    [apply funS_correct; easy | move=>> _ _; apply widen_ord_inj |].
intros i; destruct (ord_eq_dec i ord_max) as [-> | Hi].
rewrite ifF; [| destruct (pselect _)]; easy.
intros; (narrow_S Hi); rewrite widen_narrow_S; easy.
Qed.

Lemma lenPF_skip_in :
   {n} {P : 'I_n.+1 Prop} {i0},
    P i0 lenPF P = 1 + lenPF (fun iP (skip_ord i0 i)).
Proof.
intros [| n] P i0; [rewrite I_1_is_unit; intros HP;
    rewrite (lenPF1_in HP) lenPF_nil addn0; easy |].
move⇒ /asboolP HP; unfold lenPF; rewrite (cardD1x HP); f_equal.
apply sym_eq, (bijS_eq_card (skip_ord i0)), (injS_surjS_bijS I_S_is_nonempty).
apply funS_correct; intro; destruct (pselect _); [| easy].
intros _; apply /andP; split;
    [apply /asboolP; easy | apply neqP, skip_ord_correct_m].
move=>> _ _; apply skip_ord_inj.
intros i; destruct (ord_eq_dec i i0) as [-> | Hi]; move⇒ /andP.
move⇒ [_ /negP Hi]; contradict Hi; easy.
move⇒ [HP' _]; (insert_ord Hi); rewrite skip_insert_ord; easy.
Qed.

Lemma lenPF_skip_out :
   {n} {P : 'I_n.+1 Prop} {i0},
    ¬ P i0 lenPF P = lenPF (fun iP (skip_ord i0 i)).
Proof.
intros [| n] P i0 HP; [rewrite I_1_is_unit in HP;
    rewrite (lenPF1_out HP) lenPF_nil; easy |].
apply sym_eq, (bijS_eq_card (skip_ord i0)), (injS_surjS_bijS I_S_is_nonempty);
    [apply funS_correct; easy | move=>> _ _; apply skip_ord_inj |].
intros i; destruct (ord_eq_dec i i0) as [-> | Hi].
rewrite ifF; [| destruct (pselect _)]; easy.
intros; (insert_ord Hi); rewrite skip_insert_ord; easy.
Qed.

Lemma unfilterP_filterP_ord :
   {n} {P : 'I_n Prop} {i0} (HP0 : P i0) (j : 'I_(lenPF P)),
    unfilterP_ord HP0 (filterP_ord j) = j.
Proof. intros; apply enum_valK_in. Qed.

Lemma filterP_unfilterP_ord_in :
   {n} {P : 'I_n Prop} {i0} (HP0 : P i0) i,
    P i filterP_ord (unfilterP_ord HP0 i) = i.
Proof. intros; apply enum_rankK_in, in_asboolP; easy. Qed.

Lemma filterP_unfilterP_ord_in_equiv :
   {n} {P : 'I_n Prop} {i0} (HP0 : P i0) {i} (HP : P i) j,
    filterP_ord j = i j = unfilterP_ord HP0 i.
Proof.
intros; split; intros; subst.
rewrite unfilterP_filterP_ord; easy.
rewrite filterP_unfilterP_ord_in; easy.
Qed.

Lemma unfilterP_ord_out :
   {n} {P : 'I_n Prop} {i0} (HP0 : P i0) i,
    ¬ P i unfilterP_ord HP0 i = Ordinal (lenPF_n0_rev HP0).
Proof.
intros n P i0 HP0 i HP; apply val_inj;
    unfold unfilterP_ord; rewrite enum_rank_in.unlock val_insubd; simpl.
rewrite ifF; [easy | rewrite memNindex].
unfold lenPF; rewrite cardE; apply ltnn.
rewrite mem_enum; apply /negP; contradict HP; apply /asboolP; easy.
Qed.

Lemma filterP_unfilterP_ord_out :
   {n} {P : 'I_n Prop} {i0} (HP0 : P i0) i, ¬ P i
    filterP_ord (unfilterP_ord HP0 i) =
      filterP_ord (Ordinal (lenPF_n0_rev HP0)).
Proof. intros; rewrite unfilterP_ord_out; easy. Qed.

Lemma unfilterP_ord_correct_in :
   {n} {P : 'I_n Prop} {i0} (HP0 : P i0) {i},
    P i j, i = filterP_ord j unfilterP_ord HP0 i = j.
Proof.
intros n P i0 HP0 i Hi; (unfilterP_ord HP0 i); split; [| easy].
rewrite filterP_unfilterP_ord_in; easy.
Qed.

Lemma filterP_ord_correct :
   {n} (P : 'I_n Prop) (j : 'I_(lenPF P)), P (filterP_ord j).
Proof. intros n P j; generalize (enum_valP j); apply asboolW. Qed.

Lemma filterP_ord_incl_Rg :
   {n} (P : 'I_n Prop), incl P (Rg (@filterP_ord _ P)).
Proof.
move=>> Hi; destruct (unfilterP_ord_correct_in Hi Hi) as [j [-> _]]; easy.
Qed.

Lemma filterP_ord_Rg_eq :
   {n} (P : 'I_n Prop), Rg (@filterP_ord _ P) = P.
Proof.
intros; apply subset_ext_equiv; split; intro;
    [intros [j _]; apply filterP_ord_correct | apply filterP_ord_incl_Rg].
Qed.

Lemma filterP_ord_inj :
   {n} (P : 'I_n Prop),
    injective (fun j : 'I_(lenPF P)filterP_ord j).
Proof. intros; apply enum_val_inj. Qed.

Lemma unfilterP_ord_inj :
   {n} {P : 'I_n Prop} {i0} (HP0 : P i0),
     i j, P i P j
      unfilterP_ord HP0 i = unfilterP_ord HP0 j i = j.
Proof. move=>> Hi Hj; apply enum_rank_in_inj; apply /asboolP; easy. Qed.

Lemma filterP_ord_incrF_S :
   {n} (P : 'I_n Prop),
    incrF_S (fun j : 'I_(lenPF P)filterP_ord j).
Proof.
intros n P j Hj1.
apply /ltP; fold (ord_ltn (filterP_ord j) (filterP_ord (Ordinal Hj1))).
unfold filterP_ord, enum_val, enum_mem; rewrite -enumT; simpl.
move: (sorted_filter_enum_ord P) ⇒ /sorted_ordP H0.
assert (H1 : lenPF P = size (filter (fun iasbool (P i)) (enum 'I_n))).
  unfold lenPF; rewrite cardE; unfold enum_mem; do 2 f_equal.
  rewrite filter_predT; easy.
pose (jj := cast_ord H1 j).
assert (Hjj1 : jj.+1 < size (filter (fun iasbool (P i)) (enum 'I_n)))
    by now unfold jj; simpl; rewrite -H1.
apply (H0 (enum_default j) (enum_default (Ordinal Hj1)) jj Hjj1).
Qed.

Lemma filterP_ord_incrF :
   {n} (P : 'I_n Prop), incrF (fun j : 'I_(lenPF P)filterP_ord j).
Proof. intros; apply incrF_equiv, filterP_ord_incrF_S. Qed.

Lemma filterP_cast_ord_incrF :
   {m n} {P : 'I_n Prop} (H : m = lenPF P),
    incrF (filterP_ord \o (cast_ord H)).
Proof.
intros; apply incrF_comp; [apply cast_ord_incrF | apply filterP_ord_incrF].
Qed.

Lemma filterP_cast_ord_eq :
   {n m} {P : 'I_n Prop} (H1 H2 : m = lenPF P) (j : 'I_m),
    filterP_ord (cast_ord H1 j) = filterP_ord (cast_ord H2 j).
Proof.
intros [| n] m P H1 H2.
intros [j Hj]; exfalso; rewrite H1 lenPF_nil in Hj; easy.
intros; unfold filterP_ord; rewrite !(enum_val_nth ord0); easy.
Qed.

Lemma filterP_cast_ord_eq_alt :
   {n} {P Q : 'I_n Prop} (H1 H2 : lenPF P = lenPF Q) (j : 'I_(lenPF P)),
    filterP_ord (cast_ord H1 j) = filterP_ord (cast_ord H2 j).
Proof. intros; apply filterP_cast_ord_eq. Qed.

Lemma filterP_ord_ext_gen :
   {n1 n2} {Hn : n1 = n2} {P1 : 'I_n1 Prop} {P2 : 'I_n2 Prop}
      (HP : i1, P1 i1 P2 (cast_ord Hn i1)) (j1 : 'I_(lenPF P1)),
    filterP_ord j1 =
      cast_ord (sym_eq Hn) (filterP_ord (cast_ord (lenPF_ext_gen Hn HP) j1)).
Proof.
intros n1 n2 Hn P1 P2 HP j1; subst; rewrite cast_ord_id; destruct n2 as [| n2].
exfalso; destruct j1 as [j1 Hj1]; rewrite lenPF_nil in Hj1; easy.
unfold filterP_ord; rewrite !(enum_val_nth ord0); repeat f_equal.
apply fun_ext; intro; f_equal; apply prop_ext.
rewrite HP cast_ord_id; easy.
Qed.

Lemma filterP_ord_ext :
   {n} {P Q : 'I_n Prop}
      (H : i, P i Q i) (j : 'I_(lenPF P)),
    filterP_ord j = filterP_ord (cast_ord (lenPF_ext H) j).
Proof.
intros n P Q H j.
assert (H' : i, P i Q (cast_ord erefl i))
    by now intros; rewrite cast_ord_id.
rewrite (filterP_ord_ext_gen H') cast_ord_id.
repeat f_equal; apply proof_irrel.
Qed.

Lemma filterP_cast_ord :
   {n1 n2} (H : n1 = n2) {P1 : 'I_n1 Prop} {j1 : 'I_(lenPF P1)},
    filterP_ord (cast_ord (lenPF_cast_ord H P1) j1) =
      cast_ord H (filterP_ord j1).
Proof.
intros n1 n2 H P1 j1; subst.
assert (H' : i1, P1 i1 P1 (cast_ord erefl i1))
    by now intros; rewrite cast_ord_id.
rewrite cast_ord_id (filterP_ord_ext H').
repeat f_equal; apply proof_irrel.
Qed.

Lemma filterP_ord_ind_l_in_0 :
   {n} {P : 'I_n.+1 Prop} (HP : P ord0) (j : 'I_(lenPF P)),
    cast_ord (lenPF_ind_l_in HP) j = ord0 filterP_ord j = ord0.
Proof.
intros n P HP j Hj; apply (@ord0_le_equiv n.+1).
pose (f := filterP_ord \o cast_ord (sym_eq (lenPF_ind_l_in HP))).
replace (filterP_ord _) with (f ord0);
    [| unfold f; rewrite -Hj comp_correct cast_ordK; easy].
apply (incrF_cast_ord_0 (lenPF_ind_l_in HP) filterP_ord ord0);
    [apply filterP_ord_incrF | rewrite filterP_ord_Rg_eq; easy].
Qed.

Lemma filterP_ord_ind_l_in_0_rev :
   {n} {P : 'I_n.+1 Prop} (HP : P ord0) (j : 'I_(lenPF P)),
    filterP_ord j = ord0 cast_ord (lenPF_ind_l_in HP) j = ord0.
Proof.
intros n P HP j Hj.
destruct (ord_eq_dec (cast_ord (lenPF_ind_l_in HP) j) ord0)
    as [-> | Hj']; [easy | exfalso; move: Hj'].
move⇒ /(cast_ord_n0_gt_equiv (lenPF_n0_rev HP)) /filterP_ord_incrF.
rewrite Hj; easy.
Qed.

Lemma filterP_ord_ind_l_in_0_equiv :
   {n} {P : 'I_n.+1 Prop} (HP : P ord0) (j : 'I_(lenPF P)),
    filterP_ord j = ord0 cast_ord (lenPF_ind_l_in HP) j = ord0.
Proof.
intros; split;
    [apply filterP_ord_ind_l_in_0_rev | apply filterP_ord_ind_l_in_0].
Qed.

Lemma filterP_ord_ind_l_in_n0 :
   {n} {P : 'I_n.+1 Prop} (HP : P ord0)
      (j : 'I_(lenPF P)) (Hj : cast_ord (lenPF_ind_l_in HP) j ord0),
    filterP_ord j = lift_S (filterP_ord (lower_S Hj)).
Proof.
assert (H : {U1 U2 : Type} (f g : U1 U2) x1, f = g f x1 = g x1)
    by move=>> → //.
intros n P HP j Hj.
replace (filterP_ord j) with
    (filterP_ord (cast_ord (sym_eq (lenPF_ind_l_in HP)) (lift_S (lower_S Hj))))
  by now rewrite !lift_lower_S cast_ordK.
rewrite -(comp_correct (cast_ord _)) -(comp_correct lift_S (_ \o _))
    -(comp_correct filterP_ord).
apply H, fun_ext_incrF_Rg; clear j Hj.
apply incrF_comp; [apply lift_S_incrF | apply filterP_cast_ord_incrF].
apply incrF_comp; [apply filterP_ord_incrF | apply lift_S_incrF].
apply eq_trans with (fun i : 'I_n.+1i ord0 P i);
    apply subset_ext_equiv; split; unfold comp.
intros i [j _]; split; [move: (lift_S_not_first j) | apply filterP_ord_correct].
rewrite -(filterP_ord_ind_l_in_0 _
    (cast_ord (sym_eq (lenPF_ind_l_in HP)) ord0)); [| apply cast_ordKV].
rewrite -!(comp_correct _ filterP_ord); apply inj_contra.
apply inj_comp_compat; [apply cast_ord_inj | apply filterP_ord_inj].
intros i [Hi1 Hi2].
assert (Hj : cast_ord (lenPF_ind_l_in HP) (unfilterP_ord HP i) ord0).
  contradict Hi1; rewrite -(filterP_unfilterP_ord_in HP _ Hi2).
  apply (filterP_ord_ind_l_in_0 _ _ Hi1).
apply (Rg_correct (lower_S Hj));
    rewrite lift_lower_S cast_ordK filterP_unfilterP_ord_in; easy.
intros i [Hi1 Hi2].
assert (HP' : P (lift_S (lower_S Hi1))) by now rewrite lift_lower_S.
apply (Rg_correct (unfilterP_ord HP' (lower_S Hi1)));
    rewrite filterP_unfilterP_ord_in// lift_lower_S; easy.
intros i [j _]; split; [apply lift_S_not_first | apply filterP_ord_correct].
Qed.


Lemma filterP_ord_ind_l_out :
   {n} {P : 'I_n.+1 Prop} (HP : ¬ P ord0) (j : 'I_(lenPF P)),
    filterP_ord j = lift_S (filterP_ord (cast_ord (lenPF_ind_l_out HP) j)).
Proof.
intros [| n] P HP j.
exfalso; destruct j as [j Hj];
    rewrite (lenPF_ind_l_out HP) lenPF_nil in Hj; easy.
unfold filterP_ord; rewrite !(enum_val_nth ord0).
unfold enum_val, enum_mem, mem; simpl; rewrite -!enumT enum_ordSl; simpl.
unfold in_mem; simpl; case_eq (asbool (P ord0)); intros HP'.
move: HP' ⇒ /(elimT (asboolP _)) //.
rewrite filter_map (nth_map ord0); unfold lift_S; f_equal.
destruct j as [j Hj]; simpl.
replace (size _) with (lenPF (fun iP (lift ord0 i)));
    try now rewrite -lenPF_ind_l_out.
unfold lenPF; rewrite cardE; f_equal; rewrite enumT; easy.
Qed.

Lemma filterP_ord_ind_r_in_max :
   {n} {P : 'I_n.+1 Prop} (HP : P ord_max) (j : 'I_(lenPF P)),
    cast_ord (lenPF_ind_r_in_S HP) j = ord_max filterP_ord j = ord_max.
Proof.
intros n P HP j Hj; apply ord_max_ge_equiv.
pose (f := filterP_ord \o cast_ord (sym_eq (lenPF_ind_r_in_S HP))).
replace (filterP_ord _) with (f ord_max);
    [| unfold f; rewrite -Hj comp_correct cast_ordK; easy].
apply (incrF_cast_ord_max (lenPF_ind_r_in_S HP) filterP_ord ord_max);
    [apply filterP_ord_incrF | rewrite filterP_ord_Rg_eq; easy].
Qed.

Lemma filterP_ord_ind_r_in_max_rev :
   {n} {P : 'I_n.+1 Prop} (HP : P ord_max) (j : 'I_(lenPF P)),
    filterP_ord j = ord_max cast_ord (lenPF_ind_r_in_S HP) j = ord_max.
Proof.
intros n P HP j Hj.
destruct (ord_eq_dec (cast_ord (lenPF_ind_r_in_S HP) j) ord_max)
    as [-> | Hj']; [easy | exfalso; move: Hj'].
move⇒ /cast_ord_nmax_lt_equiv.
replace (j < _)%coq_nat with
    (j < cast_ord (sym_eq (lenPF_ind_r_in_S HP))
      (Ordinal (ltnSn (lenPF (fun iP (widen_S i))))))%coq_nat by easy.
move⇒ /filterP_ord_incrF; rewrite Hj filterP_ord_ind_r_in_max;
    [apply ord_lt_irrefl | apply ord_inj; easy].
Qed.

Lemma filterP_ord_ind_r_in_max_equiv :
   {n} {P : 'I_n.+1 Prop} (HP : P ord_max) (j : 'I_(lenPF P)),
    filterP_ord j = ord_max cast_ord (lenPF_ind_r_in_S HP) j = ord_max.
Proof.
intros; split;
    [apply filterP_ord_ind_r_in_max_rev | apply filterP_ord_ind_r_in_max].
Qed.

Lemma filterP_ord_ind_r_in_nmax :
   {n} {P : 'I_n.+1 Prop} (HP : P ord_max)
      (j : 'I_(lenPF P)) (Hj : cast_ord (lenPF_ind_r_in_S HP) j ord_max),
    filterP_ord j = widen_S (filterP_ord (narrow_S Hj)).
Proof.
intros [| n] P HP j Hj.
exfalso; destruct (leq_1_dec (lenPF_le P)) as [HP' | HP'].
clear Hj; destruct j as [j Hj]; rewrite HP' in Hj; easy.
contradict Hj; destruct j as [j Hj]; apply ord_inj; simpl.
rewrite HP' in Hj; rewrite lenPF_nil; apply lt_1; apply /ltP; easy.
unfold filterP_ord; rewrite !(enum_val_nth ord0) narrow_S_correct.
unfold enum_val, enum_mem, mem; simpl.
rewrite -!enumT enum_ordSr filter_rcons; simpl; unfold in_mem; simpl;
    case_eq (asbool (P ord_max)); intros HP'.
2: move: HP' ⇒ /(elimF (asboolP _)) //.
apply cast_ord_nmax_equiv in Hj; rewrite nth_rcons_l.
rewrite filter_map (nth_map ord0); unfold widen_S; f_equal.
destruct j as [j Hj1]; simpl in ×.
replace (size _) with (lenPF (fun iP (widen_S i))).
rewrite lenPF_ind_r_in_S// in Hj1; apply ltnS_neq_ltn; easy.
unfold lenPF; rewrite cardE; f_equal; rewrite enumT; easy.
replace (size _) with (lenPF (fun iP (widen_S i))); try easy.
clear j Hj; unfold lenPF; rewrite cardE; unfold enum_mem, mem; simpl.
rewrite !size_filter -!sumn_count -map_comp filter_predT; easy.
Qed.

Lemma filterP_ord_ind_r_out :
   {n} {P : 'I_n.+1 Prop} (HP : ¬ P ord_max) (j : 'I_(lenPF P)),
    filterP_ord j = widen_S (filterP_ord (cast_ord (lenPF_ind_r_out HP) j)).
Proof.
intros [| n] P HP j.
exfalso; destruct j as [j Hj].
    rewrite (lenPF_ind_r_out HP) lenPF_nil in Hj; easy.
unfold filterP_ord; rewrite !(enum_val_nth ord0).
unfold enum_val, enum_mem, mem; simpl.
rewrite -!enumT enum_ordSr filter_rcons; simpl; unfold in_mem; simpl;
    case_eq (asbool (P ord_max)); intros HP'.
move: HP' ⇒ /(elimT (asboolP _)) //.
rewrite filter_map (nth_map ord0); unfold widen_S; f_equal.
destruct j as [j Hj]; simpl.
replace (size _) with (lenPF (fun iP (widen_S i)));
    try now rewrite -lenPF_ind_r_out.
unfold lenPF; rewrite cardE; f_equal; rewrite enumT; easy.
Qed.

End FilterP_ord.