Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(*********************************************************************)

List permutations as a composition of adjacent transpositions

(*********************************************************************)

(* Adapted in May 2006 by Jean-Marc Notin from initial contents by
   Laurent Théry (Huffmann contribution, October 2003) *)

Require Import List Setoid Compare_dec Morphisms FinFun.
Import ListNotations. (* For notations [] and [a;b;c] *)
Set Implicit Arguments.
(* Set Universe Polymorphism. *)

Section Permutation.

Variable A:Type.

Inductive Permutation : list A -> list A -> Prop :=
| perm_nil: Permutation [] []
| perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l')
| perm_swap x y l : Permutation (y::x::l) (x::y::l)
| perm_trans l l' l'' :
    Permutation l l' -> Permutation l' l'' -> Permutation l l''.

Local Hint Constructors Permutation : core.

Some facts about Permutation

Theorem Permutation_nil : forall (l : list A), Permutation [] l -> l = [].A:Type
forall l : list A, Permutation [] l -> l = []
Proof.A:Type
forall l : list A, Permutation [] l -> l = []
  intros l HF.A:Type
l:list A
HF:Permutation [] l
l = []
  remember (@nil A) as m in HF.A:Type
l, m:list A
Heqm:m = []
HF:Permutation m l
l = []
  induction HF; discriminate || auto.
Qed.

Theorem Permutation_nil_cons : forall (l : list A) (x : A),
 ~ Permutation nil (x::l).A:Type
forall (l : list A) (x : A), ~ Permutation [] (x :: l)
Proof.A:Type
forall (l : list A) (x : A), ~ Permutation [] (x :: l)
  intros l x HF.A:Type
l:list A
x:A
HF:Permutation [] (x :: l)
False
  apply Permutation_nil in HF; discriminate.
Qed.

Permutation over lists is a equivalence relation

Theorem Permutation_refl : forall l : list A, Permutation l l.A:Type
forall l : list A, Permutation l l
Proof.A:Type
forall l : list A, Permutation l l
  induction l; constructor.A:Type
a:A
l:list A
IHl:Permutation l l
Permutation l l exact IHl.
Qed.

Theorem Permutation_sym : forall l l' : list A,
 Permutation l l' -> Permutation l' l.A:Type
forall l l' : list A,
Permutation l l' -> Permutation l' l
Proof.A:Type
forall l l' : list A,
Permutation l l' -> Permutation l' l
  intros l l' Hperm; induction Hperm; auto.A:Type
l, l', l'':list A
Hperm1:Permutation l l'
Hperm2:Permutation l' l''
IHHperm1:Permutation l' l
IHHperm2:Permutation l'' l'
Permutation l'' l
  apply perm_trans with (l':=l'); assumption.
Qed.

Theorem Permutation_trans : forall l l' l'' : list A,
 Permutation l l' -> Permutation l' l'' -> Permutation l l''.A:Type
forall l l' l'' : list A,
Permutation l l' ->
Permutation l' l'' -> Permutation l l''
Proof.A:Type
forall l l' l'' : list A,
Permutation l l' ->
Permutation l' l'' -> Permutation l l''
  exact perm_trans.
Qed.

End Permutation.

Hint Resolve Permutation_refl perm_nil perm_skip : core.

(* These hints do not reduce the size of the problem to solve and they
   must be used with care to avoid combinatoric explosions *)

Local Hint Resolve perm_swap perm_trans : core.
Local Hint Resolve Permutation_sym Permutation_trans : core.

(* This provides reflexivity, symmetry and transitivity and rewriting
   on morphims to come *)

Instance Permutation_Equivalence A : Equivalence (@Permutation A) | 10 := {
  Equivalence_Reflexive := @Permutation_refl A ;
  Equivalence_Symmetric := @Permutation_sym A ;
  Equivalence_Transitive := @Permutation_trans A }.

Instance Permutation_cons A :
 Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A) | 10.A:Type
Proper
  (eq ==> Permutation (A:=A) ==> Permutation (A:=A))
  cons
Proof.A:Type
Proper
  (eq ==> Permutation (A:=A) ==> Permutation (A:=A))
  cons
  repeat intro; subst; auto using perm_skip.
Qed.

Section Permutation_properties.

Variable A:Type.

Implicit Types a b : A.
Implicit Types l m : list A.

Compatibility with others operations on lists

Theorem Permutation_in : forall (l l' : list A) (x : A),
 Permutation l l' -> In x l -> In x l'.A:Type
forall (l l' : list A) (x : A),
Permutation l l' -> In x l -> In x l'
Proof.A:Type
forall (l l' : list A) (x : A),
Permutation l l' -> In x l -> In x l'
  intros l l' x Hperm; induction Hperm; simpl; tauto.
Qed.

Instance Permutation_in' :
 Proper (Logic.eq ==> @Permutation A ==> iff) (@In A) | 10.A:Type
Proper (eq ==> Permutation (A:=A) ==> iff) (In (A:=A))
Proof.A:Type
Proper (eq ==> Permutation (A:=A) ==> iff) (In (A:=A))
  repeat red; intros; subst; eauto using Permutation_in.
Qed.

Lemma Permutation_app_tail : forall (l l' tl : list A),
 Permutation l l' -> Permutation (l++tl) (l'++tl).A:Type
forall l l' tl : list A,
Permutation l l' -> Permutation (l ++ tl) (l' ++ tl)
Proof.A:Type
forall l l' tl : list A,
Permutation l l' -> Permutation (l ++ tl) (l' ++ tl)
  intros l l' tl Hperm; induction Hperm as [|x l l'|x y l|l l' l'']; simpl; auto.A:Type
tl, l, l', l'':list A
Hperm1:Permutation l l'
Hperm2:Permutation l' l''
IHHperm1:Permutation (l ++ tl) (l' ++ tl)
IHHperm2:Permutation (l' ++ tl) (l'' ++ tl)
Permutation (l ++ tl) (l'' ++ tl)
  eapply Permutation_trans with (l':=l'++tl); trivial.
Qed.

Lemma Permutation_app_head : forall (l tl tl' : list A),
 Permutation tl tl' -> Permutation (l++tl) (l++tl').A:Type
forall l tl tl' : list A,
Permutation tl tl' -> Permutation (l ++ tl) (l ++ tl')
Proof.A:Type
forall l tl tl' : list A,
Permutation tl tl' -> Permutation (l ++ tl) (l ++ tl')
  intros l tl tl' Hperm; induction l;
   [trivial | repeat rewrite <- app_comm_cons; constructor; assumption].
Qed.

Theorem Permutation_app : forall (l m l' m' : list A),
 Permutation l l' -> Permutation m m' -> Permutation (l++m) (l'++m').A:Type
forall l m l' m' : list A,
Permutation l l' ->
Permutation m m' -> Permutation (l ++ m) (l' ++ m')
Proof.A:Type
forall l m l' m' : list A,
Permutation l l' ->
Permutation m m' -> Permutation (l ++ m) (l' ++ m')
  intros l m l' m' Hpermll' Hpermmm';
   induction Hpermll' as [|x l l'|x y l|l l' l''];
    repeat rewrite <- app_comm_cons; auto.A:Type
m, m':list A
x, y:A
l:list A
Hpermmm':Permutation m m'
Permutation (y :: x :: l ++ m) (x :: y :: l ++ m')
A:Type
m, m', l, l', l'':list A
Hpermll'1:Permutation l l'
Hpermll'2:Permutation l' l''
Hpermmm':Permutation m m'
IHHpermll'1:Permutation (l ++ m) (l' ++ m')
IHHpermll'2:Permutation (l' ++ m) (l'' ++ m')
Permutation (l ++ m) (l'' ++ m')
  apply Permutation_trans with (l' := (x :: y :: l ++ m));
   [idtac | repeat rewrite app_comm_cons; apply Permutation_app_head]; trivial.A:Type
m, m', l, l', l'':list A
Hpermll'1:Permutation l l'
Hpermll'2:Permutation l' l''
Hpermmm':Permutation m m'
IHHpermll'1:Permutation (l ++ m) (l' ++ m')
IHHpermll'2:Permutation (l' ++ m) (l'' ++ m')
Permutation (l ++ m) (l'' ++ m')
  apply Permutation_trans with (l' := (l' ++ m')); try assumption.A:Type
m, m', l, l', l'':list A
Hpermll'1:Permutation l l'
Hpermll'2:Permutation l' l''
Hpermmm':Permutation m m'
IHHpermll'1:Permutation (l ++ m) (l' ++ m')
IHHpermll'2:Permutation (l' ++ m) (l'' ++ m')
Permutation (l' ++ m') (l'' ++ m')
  apply Permutation_app_tail; assumption.
Qed.

Instance Permutation_app' :
 Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A) | 10.A:Type
Proper
  (Permutation (A:=A) ==>
   Permutation (A:=A) ==> Permutation (A:=A))
  (app (A:=A))
Proof.A:Type
Proper
  (Permutation (A:=A) ==>
   Permutation (A:=A) ==> Permutation (A:=A))
  (app (A:=A))
  repeat intro; now apply Permutation_app.
Qed.

Lemma Permutation_add_inside : forall a (l l' tl tl' : list A),
  Permutation l l' -> Permutation tl tl' ->
  Permutation (l ++ a :: tl) (l' ++ a :: tl').A:Type
forall (a : A) (l l' tl tl' : list A),
Permutation l l' ->
Permutation tl tl' ->
Permutation (l ++ a :: tl) (l' ++ a :: tl')
Proof.A:Type
forall (a : A) (l l' tl tl' : list A),
Permutation l l' ->
Permutation tl tl' ->
Permutation (l ++ a :: tl) (l' ++ a :: tl')
  intros; apply Permutation_app; auto.
Qed.

Lemma Permutation_cons_append : forall (l : list A) x,
  Permutation (x :: l) (l ++ x :: nil).A:Type
forall (l : list A) (x : A),
Permutation (x :: l) (l ++ [x])
Proof.A:Type
forall (l : list A) (x : A),
Permutation (x :: l) (l ++ [x]) induction l; intros; auto.A:Type
a:A
l:list A
IHl:forall x0 : A, Permutation (x0 :: l) (l ++ [x0])
x:A
Permutation (x :: a :: l) ((a :: l) ++ [x]) simpl.A:Type
a:A
l:list A
IHl:forall x0 : A, Permutation (x0 :: l) (l ++ [x0])
x:A
Permutation (x :: a :: l) (a :: l ++ [x]) rewrite <- IHl; auto. Qed.
Local Hint Resolve Permutation_cons_append : core.

Theorem Permutation_app_comm : forall (l l' : list A),
  Permutation (l ++ l') (l' ++ l).A:Type
forall l l' : list A, Permutation (l ++ l') (l' ++ l)
Proof.A:Type
forall l l' : list A, Permutation (l ++ l') (l' ++ l)
  induction l as [|x l]; simpl; intro l'.A:Type
l':list A
Permutation l' (l' ++ [])
A:Type
x:A
l:list A
IHl:forall l'0 : list A, Permutation (l ++ l'0) (l'0 ++ l)
l':list A
Permutation (x :: l ++ l') (l' ++ x :: l)
  rewrite app_nil_r; trivial.A:Type
x:A
l:list A
IHl:forall l'0 : list A, Permutation (l ++ l'0) (l'0 ++ l)
l':list A
Permutation (x :: l ++ l') (l' ++ x :: l) rewrite IHl.A:Type
x:A
l:list A
IHl:forall l'0 : list A, Permutation (l ++ l'0) (l'0 ++ l)
l':list A
Permutation (x :: l' ++ l) (l' ++ x :: l)
  rewrite app_comm_cons, Permutation_cons_append.A:Type
x:A
l:list A
IHl:forall l'0 : list A, Permutation (l ++ l'0) (l'0 ++ l)
l':list A
Permutation ((l' ++ [x]) ++ l) (l' ++ x :: l)
  now rewrite <- app_assoc.
Qed.
Local Hint Resolve Permutation_app_comm : core.

Theorem Permutation_cons_app : forall (l l1 l2:list A) a,
  Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).A:Type
forall (l l1 l2 : list A) (a : A),
Permutation l (l1 ++ l2) ->
Permutation (a :: l) (l1 ++ a :: l2)
Proof.A:Type
forall (l l1 l2 : list A) (a : A),
Permutation l (l1 ++ l2) ->
Permutation (a :: l) (l1 ++ a :: l2)
  intros l l1 l2 a H.A:Type
l, l1, l2:list A
a:A
H:Permutation l (l1 ++ l2)
Permutation (a :: l) (l1 ++ a :: l2) rewrite H.A:Type
l, l1, l2:list A
a:A
H:Permutation l (l1 ++ l2)
Permutation (a :: l1 ++ l2) (l1 ++ a :: l2)
  rewrite app_comm_cons, Permutation_cons_append.A:Type
l, l1, l2:list A
a:A
H:Permutation l (l1 ++ l2)
Permutation ((l1 ++ [a]) ++ l2) (l1 ++ a :: l2)
  now rewrite <- app_assoc.
Qed.
Local Hint Resolve Permutation_cons_app : core.

Lemma Permutation_Add a l l' : Add a l l' -> Permutation (a::l) l'.A:Type
a:A
l, l':list A
Add a l l' -> Permutation (a :: l) l'
Proof.A:Type
a:A
l, l':list A
Add a l l' -> Permutation (a :: l) l'
 induction 1; simpl; trivial.A:Type
a, x:A
l, l':list A
H:Add a l l'
IHAdd:Permutation (a :: l) l'
Permutation (a :: x :: l) (x :: l')
 rewrite perm_swap.A:Type
a, x:A
l, l':list A
H:Add a l l'
IHAdd:Permutation (a :: l) l'
Permutation (x :: a :: l) (x :: l') now apply perm_skip.
Qed.

Theorem Permutation_middle : forall (l1 l2:list A) a,
  Permutation (a :: l1 ++ l2) (l1 ++ a :: l2).A:Type
forall (l1 l2 : list A) (a : A),
Permutation (a :: l1 ++ l2) (l1 ++ a :: l2)
Proof.A:Type
forall (l1 l2 : list A) (a : A),
Permutation (a :: l1 ++ l2) (l1 ++ a :: l2)
  auto.
Qed.
Local Hint Resolve Permutation_middle : core.

Theorem Permutation_rev : forall (l : list A), Permutation l (rev l).A:Type
forall l : list A, Permutation l (rev l)
Proof.A:Type
forall l : list A, Permutation l (rev l)
  induction l as [| x l]; simpl; trivial.A:Type
x:A
l:list A
IHl:Permutation l (rev l)
Permutation (x :: l) (rev l ++ [x]) now rewrite IHl at 1.
Qed.

Instance Permutation_rev' :
 Proper (@Permutation A ==> @Permutation A) (@rev A) | 10.A:Type
Proper (Permutation (A:=A) ==> Permutation (A:=A))
  (rev (A:=A))
Proof.A:Type
Proper (Permutation (A:=A) ==> Permutation (A:=A))
  (rev (A:=A))
  repeat intro; now rewrite <- 2 Permutation_rev.
Qed.

Theorem Permutation_length : forall (l l' : list A),
 Permutation l l' -> length l = length l'.A:Type
forall l l' : list A,
Permutation l l' -> length l = length l'
Proof.A:Type
forall l l' : list A,
Permutation l l' -> length l = length l'
  intros l l' Hperm; induction Hperm; simpl; auto.A:Type
l, l', l'':list A
Hperm1:Permutation l l'
Hperm2:Permutation l' l''
IHHperm1:length l = length l'
IHHperm2:length l' = length l''
length l = length l'' now transitivity (length l').
Qed.

Instance Permutation_length' :
 Proper (@Permutation A ==> Logic.eq) (@length A) | 10.A:Type
Proper (Permutation (A:=A) ==> eq) (length (A:=A))
Proof.A:Type
Proper (Permutation (A:=A) ==> eq) (length (A:=A))
  exact Permutation_length.
Qed.

Theorem Permutation_ind_bis :
 forall P : list A -> list A -> Prop,
   P [] [] ->
   (forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) ->
   (forall x y l l', Permutation l l' -> P l l' -> P (y :: x :: l) (x :: y :: l')) ->
   (forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') ->
   forall l l', Permutation l l' -> P l l'.A:Type
forall P : list A -> list A -> Prop,
P [] [] ->
(forall (x : A) (l l' : list A),
 Permutation l l' -> P l l' -> P (x :: l) (x :: l')) ->
(forall (x y : A) (l l' : list A),
 Permutation l l' ->
 P l l' -> P (y :: x :: l) (x :: y :: l')) ->
(forall l l' l'' : list A,
 Permutation l l' ->
 P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') ->
forall l l' : list A, Permutation l l' -> P l l'
Proof.A:Type
forall P : list A -> list A -> Prop,
P [] [] ->
(forall (x : A) (l l' : list A),
 Permutation l l' -> P l l' -> P (x :: l) (x :: l')) ->
(forall (x y : A) (l l' : list A),
 Permutation l l' ->
 P l l' -> P (y :: x :: l) (x :: y :: l')) ->
(forall l l' l'' : list A,
 Permutation l l' ->
 P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') ->
forall l l' : list A, Permutation l l' -> P l l'
  intros P Hnil Hskip Hswap Htrans.A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x : A) (l l' : list A),
Permutation l l' ->
P l l' -> P (x :: l) (x :: l')
Hswap:forall (x y : A) (l l' : list A),
Permutation l l' ->
P l l' -> P (y :: x :: l) (x :: y :: l')
Htrans:forall l l' l'' : list A,
Permutation l l' ->
P l l' ->
Permutation l' l'' -> P l' l'' -> P l l''
forall l l' : list A, Permutation l l' -> P l l'
  induction 1; auto.A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (x0 :: l0) (x0 :: l')
Hswap:forall (x0 y0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (y0 :: x0 :: l0) (x0 :: y0 :: l')
Htrans:forall l0 l' l'' : list A,
Permutation l0 l' ->
P l0 l' ->
Permutation l' l'' -> P l' l'' -> P l0 l''
x, y:A
l:list A
P (y :: x :: l) (x :: y :: l)
A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x : A) (l0 l'0 : list A),
Permutation l0 l'0 ->
P l0 l'0 -> P (x :: l0) (x :: l'0)
Hswap:forall (x y : A) (l0 l'0 : list A),
Permutation l0 l'0 ->
P l0 l'0 -> P (y :: x :: l0) (x :: y :: l'0)
Htrans:forall l0 l'0 l''0 : list A,
Permutation l0 l'0 ->
P l0 l'0 ->
Permutation l'0 l''0 ->
P l'0 l''0 -> P l0 l''0
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:P l l'
IHPermutation2:P l' l''
P l l''
  apply Htrans with (x::y::l); auto.A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (x0 :: l0) (x0 :: l')
Hswap:forall (x0 y0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (y0 :: x0 :: l0) (x0 :: y0 :: l')
Htrans:forall l0 l' l'' : list A,
Permutation l0 l' ->
P l0 l' ->
Permutation l' l'' -> P l' l'' -> P l0 l''
x, y:A
l:list A
P (y :: x :: l) (x :: y :: l)
A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (x0 :: l0) (x0 :: l')
Hswap:forall (x0 y0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (y0 :: x0 :: l0) (x0 :: y0 :: l')
Htrans:forall l0 l' l'' : list A,
Permutation l0 l' ->
P l0 l' ->
Permutation l' l'' -> P l' l'' -> P l0 l''
x, y:A
l:list A
P (x :: y :: l) (x :: y :: l)
A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x : A) (l0 l'0 : list A),
Permutation l0 l'0 ->
P l0 l'0 -> P (x :: l0) (x :: l'0)
Hswap:forall (x y : A) (l0 l'0 : list A),
Permutation l0 l'0 ->
P l0 l'0 -> P (y :: x :: l0) (x :: y :: l'0)
Htrans:forall l0 l'0 l''0 : list A,
Permutation l0 l'0 ->
P l0 l'0 ->
Permutation l'0 l''0 ->
P l'0 l''0 -> P l0 l''0
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:P l l'
IHPermutation2:P l' l''
P l l''
  apply Hswap; auto.A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (x0 :: l0) (x0 :: l')
Hswap:forall (x0 y0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (y0 :: x0 :: l0) (x0 :: y0 :: l')
Htrans:forall l0 l' l'' : list A,
Permutation l0 l' ->
P l0 l' ->
Permutation l' l'' -> P l' l'' -> P l0 l''
x, y:A
l:list A
P l l
A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (x0 :: l0) (x0 :: l')
Hswap:forall (x0 y0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (y0 :: x0 :: l0) (x0 :: y0 :: l')
Htrans:forall l0 l' l'' : list A,
Permutation l0 l' ->
P l0 l' ->
Permutation l' l'' -> P l' l'' -> P l0 l''
x, y:A
l:list A
P (x :: y :: l) (x :: y :: l)
A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x : A) (l0 l'0 : list A),
Permutation l0 l'0 ->
P l0 l'0 -> P (x :: l0) (x :: l'0)
Hswap:forall (x y : A) (l0 l'0 : list A),
Permutation l0 l'0 ->
P l0 l'0 -> P (y :: x :: l0) (x :: y :: l'0)
Htrans:forall l0 l'0 l''0 : list A,
Permutation l0 l'0 ->
P l0 l'0 ->
Permutation l'0 l''0 ->
P l'0 l''0 -> P l0 l''0
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:P l l'
IHPermutation2:P l' l''
P l l''
  induction l; auto.A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (x0 :: l0) (x0 :: l')
Hswap:forall (x0 y0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (y0 :: x0 :: l0) (x0 :: y0 :: l')
Htrans:forall l0 l' l'' : list A,
Permutation l0 l' ->
P l0 l' ->
Permutation l' l'' -> P l' l'' -> P l0 l''
x, y:A
l:list A
P (x :: y :: l) (x :: y :: l)
A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x : A) (l0 l'0 : list A),
Permutation l0 l'0 ->
P l0 l'0 -> P (x :: l0) (x :: l'0)
Hswap:forall (x y : A) (l0 l'0 : list A),
Permutation l0 l'0 ->
P l0 l'0 -> P (y :: x :: l0) (x :: y :: l'0)
Htrans:forall l0 l'0 l''0 : list A,
Permutation l0 l'0 ->
P l0 l'0 ->
Permutation l'0 l''0 ->
P l'0 l''0 -> P l0 l''0
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:P l l'
IHPermutation2:P l' l''
P l l''
  apply Hskip; auto.A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (x0 :: l0) (x0 :: l')
Hswap:forall (x0 y0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (y0 :: x0 :: l0) (x0 :: y0 :: l')
Htrans:forall l0 l' l'' : list A,
Permutation l0 l' ->
P l0 l' ->
Permutation l' l'' -> P l' l'' -> P l0 l''
x, y:A
l:list A
P (y :: l) (y :: l)
A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x : A) (l0 l'0 : list A),
Permutation l0 l'0 ->
P l0 l'0 -> P (x :: l0) (x :: l'0)
Hswap:forall (x y : A) (l0 l'0 : list A),
Permutation l0 l'0 ->
P l0 l'0 -> P (y :: x :: l0) (x :: y :: l'0)
Htrans:forall l0 l'0 l''0 : list A,
Permutation l0 l'0 ->
P l0 l'0 ->
Permutation l'0 l''0 ->
P l'0 l''0 -> P l0 l''0
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:P l l'
IHPermutation2:P l' l''
P l l''
  apply Hskip; auto.A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (x0 :: l0) (x0 :: l')
Hswap:forall (x0 y0 : A) (l0 l' : list A),
Permutation l0 l' ->
P l0 l' -> P (y0 :: x0 :: l0) (x0 :: y0 :: l')
Htrans:forall l0 l' l'' : list A,
Permutation l0 l' ->
P l0 l' ->
Permutation l' l'' -> P l' l'' -> P l0 l''
x, y:A
l:list A
P l l
A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x : A) (l0 l'0 : list A),
Permutation l0 l'0 ->
P l0 l'0 -> P (x :: l0) (x :: l'0)
Hswap:forall (x y : A) (l0 l'0 : list A),
Permutation l0 l'0 ->
P l0 l'0 -> P (y :: x :: l0) (x :: y :: l'0)
Htrans:forall l0 l'0 l''0 : list A,
Permutation l0 l'0 ->
P l0 l'0 ->
Permutation l'0 l''0 ->
P l'0 l''0 -> P l0 l''0
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:P l l'
IHPermutation2:P l' l''
P l l''
  induction l; auto.A:Type
P:list A -> list A -> Prop
Hnil:P [] []
Hskip:forall (x : A) (l0 l'0 : list A),
Permutation l0 l'0 ->
P l0 l'0 -> P (x :: l0) (x :: l'0)
Hswap:forall (x y : A) (l0 l'0 : list A),
Permutation l0 l'0 ->
P l0 l'0 -> P (y :: x :: l0) (x :: y :: l'0)
Htrans:forall l0 l'0 l''0 : list A,
Permutation l0 l'0 ->
P l0 l'0 ->
Permutation l'0 l''0 ->
P l'0 l''0 -> P l0 l''0
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:P l l'
IHPermutation2:P l' l''
P l l''
  eauto.
Qed.

Theorem Permutation_nil_app_cons : forall (l l' : list A) (x : A),
 ~ Permutation nil (l++x::l').A:Type
forall (l l' : list A) (x : A),
~ Permutation [] (l ++ x :: l')
Proof.A:Type
forall (l l' : list A) (x : A),
~ Permutation [] (l ++ x :: l')
  intros l l' x HF.A:Type
l, l':list A
x:A
HF:Permutation [] (l ++ x :: l')
False
  apply Permutation_nil in HF.A:Type
l, l':list A
x:A
HF:l ++ x :: l' = []
False destruct l; discriminate.
Qed.

Ltac InvAdd := repeat (match goal with
 | H: Add ?x _ (_ :: _) |- _ => inversion H; clear H; subst
 end).

Ltac finish_basic_perms H :=
  try constructor; try rewrite perm_swap; try constructor; trivial;
  (rewrite <- H; now apply Permutation_Add) ||
  (rewrite H; symmetry; now apply Permutation_Add).

Theorem Permutation_Add_inv a l1 l2 :
  Permutation l1 l2 -> forall l1' l2', Add a l1' l1 -> Add a l2' l2 ->
   Permutation l1' l2'.A:Type
a:A
l1, l2:list A
Permutation l1 l2 ->
forall l1' l2' : list A,
Add a l1' l1 -> Add a l2' l2 -> Permutation l1' l2'
Proof.A:Type
a:A
l1, l2:list A
Permutation l1 l2 ->
forall l1' l2' : list A,
Add a l1' l1 -> Add a l2' l2 -> Permutation l1' l2'
 revert l1 l2.A:Type
a:A
forall l1 l2 : list A,
Permutation l1 l2 ->
forall l1' l2' : list A,
Add a l1' l1 -> Add a l2' l2 -> Permutation l1' l2' refine (Permutation_ind_bis _ _ _ _ _).A:Type
a:A
forall l1' l2' : list A,
Add a l1' [] -> Add a l2' [] -> Permutation l1' l2'
A:Type
a:A
forall (x : A) (l l' : list A),
Permutation l l' ->
(forall l1' l2' : list A,
 Add a l1' l -> Add a l2' l' -> Permutation l1' l2') ->
forall l1' l2' : list A,
Add a l1' (x :: l) ->
Add a l2' (x :: l') -> Permutation l1' l2'
A:Type
a:A
forall (x y : A) (l l' : list A),
Permutation l l' ->
(forall l1' l2' : list A,
 Add a l1' l -> Add a l2' l' -> Permutation l1' l2') ->
forall l1' l2' : list A,
Add a l1' (y :: x :: l) ->
Add a l2' (x :: y :: l') -> Permutation l1' l2'
A:Type
a:A
forall l l' l'' : list A,
Permutation l l' ->
(forall l1' l2' : list A,
 Add a l1' l -> Add a l2' l' -> Permutation l1' l2') ->
Permutation l' l'' ->
(forall l1' l2' : list A,
 Add a l1' l' -> Add a l2' l'' -> Permutation l1' l2') ->
forall l1' l2' : list A,
Add a l1' l -> Add a l2' l'' -> Permutation l1' l2'
 - (* nil *)A:Type
a:A
forall l1' l2' : list A,
Add a l1' [] -> Add a l2' [] -> Permutation l1' l2'
   inversion_clear 1.
 - (* skip *)A:Type
a:A
forall (x : A) (l l' : list A),
Permutation l l' ->
(forall l1' l2' : list A,
 Add a l1' l -> Add a l2' l' -> Permutation l1' l2') ->
forall l1' l2' : list A,
Add a l1' (x :: l) ->
Add a l2' (x :: l') -> Permutation l1' l2'
   intros x l1 l2 PE IH.A:Type
a, x:A
l1, l2:list A
PE:Permutation l1 l2
IH:forall l1' l2' : list A,
Add a l1' l1 ->
Add a l2' l2 -> Permutation l1' l2'
forall l1' l2' : list A,
Add a l1' (x :: l1) ->
Add a l2' (x :: l2) -> Permutation l1' l2' intros.A:Type
a, x:A
l1, l2:list A
PE:Permutation l1 l2
IH:forall l1'0 l2'0 : list A,
Add a l1'0 l1 ->
Add a l2'0 l2 -> Permutation l1'0 l2'0
l1', l2':list A
H:Add a l1' (x :: l1)
H0:Add a l2' (x :: l2)
Permutation l1' l2' InvAdd; try finish_basic_perms PE.A:Type
a, x:A
l1, l2:list A
PE:Permutation l1 l2
IH:forall l1' l2' : list A,
Add a l1' l1 ->
Add a l2' l2 -> Permutation l1' l2'
l:list A
H3:Add a l l2
l0:list A
H2:Add a l0 l1
Permutation (x :: l0) (x :: l)
   constructor.A:Type
a, x:A
l1, l2:list A
PE:Permutation l1 l2
IH:forall l1' l2' : list A,
Add a l1' l1 ->
Add a l2' l2 -> Permutation l1' l2'
l:list A
H3:Add a l l2
l0:list A
H2:Add a l0 l1
Permutation l0 l now apply IH.
 - (* swap *)A:Type
a:A
forall (x y : A) (l l' : list A),
Permutation l l' ->
(forall l1' l2' : list A,
 Add a l1' l -> Add a l2' l' -> Permutation l1' l2') ->
forall l1' l2' : list A,
Add a l1' (y :: x :: l) ->
Add a l2' (x :: y :: l') -> Permutation l1' l2'
   intros x y l1 l2 PE IH.A:Type
a, x, y:A
l1, l2:list A
PE:Permutation l1 l2
IH:forall l1' l2' : list A,
Add a l1' l1 ->
Add a l2' l2 -> Permutation l1' l2'
forall l1' l2' : list A,
Add a l1' (y :: x :: l1) ->
Add a l2' (x :: y :: l2) -> Permutation l1' l2' intros.A:Type
a, x, y:A
l1, l2:list A
PE:Permutation l1 l2
IH:forall l1'0 l2'0 : list A,
Add a l1'0 l1 ->
Add a l2'0 l2 -> Permutation l1'0 l2'0
l1', l2':list A
H:Add a l1' (y :: x :: l1)
H0:Add a l2' (x :: y :: l2)
Permutation l1' l2' InvAdd; try finish_basic_perms PE.A:Type
a, x, y:A
l1, l2:list A
PE:Permutation l1 l2
IH:forall l1' l2' : list A,
Add a l1' l1 ->
Add a l2' l2 -> Permutation l1' l2'
l0:list A
H2:Add a l0 l2
l3:list A
H1:Add a l3 l1
Permutation (y :: x :: l3) (x :: y :: l0)
   rewrite perm_swap; do 2 constructor.A:Type
a, x, y:A
l1, l2:list A
PE:Permutation l1 l2
IH:forall l1' l2' : list A,
Add a l1' l1 ->
Add a l2' l2 -> Permutation l1' l2'
l0:list A
H2:Add a l0 l2
l3:list A
H1:Add a l3 l1
Permutation l3 l0 now apply IH.
 - (* trans *)A:Type
a:A
forall l l' l'' : list A,
Permutation l l' ->
(forall l1' l2' : list A,
 Add a l1' l -> Add a l2' l' -> Permutation l1' l2') ->
Permutation l' l'' ->
(forall l1' l2' : list A,
 Add a l1' l' -> Add a l2' l'' -> Permutation l1' l2') ->
forall l1' l2' : list A,
Add a l1' l -> Add a l2' l'' -> Permutation l1' l2'
   intros l1 l l2 PE IH PE' IH' l1' l2' AD1 AD2.A:Type
a:A
l1, l, l2:list A
PE:Permutation l1 l
IH:forall l1'0 l2'0 : list A,
Add a l1'0 l1 ->
Add a l2'0 l -> Permutation l1'0 l2'0
PE':Permutation l l2
IH':forall l1'0 l2'0 : list A,
Add a l1'0 l -> Add a l2'0 l2 -> Permutation l1'0 l2'0
l1', l2':list A
AD1:Add a l1' l1
AD2:Add a l2' l2
Permutation l1' l2'
   assert (Ha : In a l).A:Type
a:A
l1, l, l2:list A
PE:Permutation l1 l
IH:forall l1'0 l2'0 : list A,
Add a l1'0 l1 ->
Add a l2'0 l -> Permutation l1'0 l2'0
PE':Permutation l l2
IH':forall l1'0 l2'0 : list A,
Add a l1'0 l -> Add a l2'0 l2 -> Permutation l1'0 l2'0
l1', l2':list A
AD1:Add a l1' l1
AD2:Add a l2' l2
In a l
A:Type
a:A
l1, l, l2:list A
PE:Permutation l1 l
IH:forall l1'0 l2'0 : list A,
Add a l1'0 l1 ->
Add a l2'0 l -> Permutation l1'0 l2'0
PE':Permutation l l2
IH':forall l1'0 l2'0 : list A,
Add a l1'0 l -> Add a l2'0 l2 -> Permutation l1'0 l2'0
l1', l2':list A
AD1:Add a l1' l1
AD2:Add a l2' l2
Ha:In a l
Permutation l1' l2' {A:Type
a:A
l1, l, l2:list A
PE:Permutation l1 l
IH:forall l1'0 l2'0 : list A,
Add a l1'0 l1 ->
Add a l2'0 l -> Permutation l1'0 l2'0
PE':Permutation l l2
IH':forall l1'0 l2'0 : list A,
Add a l1'0 l -> Add a l2'0 l2 -> Permutation l1'0 l2'0
l1', l2':list A
AD1:Add a l1' l1
AD2:Add a l2' l2
In a l rewrite <- PE.A:Type
a:A
l1, l, l2:list A
PE:Permutation l1 l
IH:forall l1'0 l2'0 : list A,
Add a l1'0 l1 ->
Add a l2'0 l -> Permutation l1'0 l2'0
PE':Permutation l l2
IH':forall l1'0 l2'0 : list A,
Add a l1'0 l -> Add a l2'0 l2 -> Permutation l1'0 l2'0
l1', l2':list A
AD1:Add a l1' l1
AD2:Add a l2' l2
In a l1 rewrite (Add_in AD1).A:Type
a:A
l1, l, l2:list A
PE:Permutation l1 l
IH:forall l1'0 l2'0 : list A,
Add a l1'0 l1 ->
Add a l2'0 l -> Permutation l1'0 l2'0
PE':Permutation l l2
IH':forall l1'0 l2'0 : list A,
Add a l1'0 l -> Add a l2'0 l2 -> Permutation l1'0 l2'0
l1', l2':list A
AD1:Add a l1' l1
AD2:Add a l2' l2
In a (a :: l1') simpl; auto. }A:Type
a:A
l1, l, l2:list A
PE:Permutation l1 l
IH:forall l1'0 l2'0 : list A,
Add a l1'0 l1 ->
Add a l2'0 l -> Permutation l1'0 l2'0
PE':Permutation l l2
IH':forall l1'0 l2'0 : list A,
Add a l1'0 l -> Add a l2'0 l2 -> Permutation l1'0 l2'0
l1', l2':list A
AD1:Add a l1' l1
AD2:Add a l2' l2
Ha:In a l
Permutation l1' l2'
   destruct (Add_inv _ _ Ha) as (l',AD).A:Type
a:A
l1, l, l2:list A
PE:Permutation l1 l
IH:forall l1'0 l2'0 : list A,
Add a l1'0 l1 ->
Add a l2'0 l -> Permutation l1'0 l2'0
PE':Permutation l l2
IH':forall l1'0 l2'0 : list A,
Add a l1'0 l -> Add a l2'0 l2 -> Permutation l1'0 l2'0
l1', l2':list A
AD1:Add a l1' l1
AD2:Add a l2' l2
Ha:In a l
l':list A
AD:Add a l' l
Permutation l1' l2'
   transitivity l'; auto.
Qed.

Theorem Permutation_app_inv (l1 l2 l3 l4:list A) a :
  Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4).A:Type
l1, l2, l3, l4:list A
a:A
Permutation (l1 ++ a :: l2) (l3 ++ a :: l4) ->
Permutation (l1 ++ l2) (l3 ++ l4)
Proof.A:Type
l1, l2, l3, l4:list A
a:A
Permutation (l1 ++ a :: l2) (l3 ++ a :: l4) ->
Permutation (l1 ++ l2) (l3 ++ l4)
 intros.A:Type
l1, l2, l3, l4:list A
a:A
H:Permutation (l1 ++ a :: l2) (l3 ++ a :: l4)
Permutation (l1 ++ l2) (l3 ++ l4) eapply Permutation_Add_inv; eauto using Add_app.
Qed.

Theorem Permutation_cons_inv l l' a :
 Permutation (a::l) (a::l') -> Permutation l l'.A:Type
l, l':list A
a:A
Permutation (a :: l) (a :: l') -> Permutation l l'
Proof.A:Type
l, l':list A
a:A
Permutation (a :: l) (a :: l') -> Permutation l l'
  intro.A:Type
l, l':list A
a:A
H:Permutation (a :: l) (a :: l')
Permutation l l' eapply Permutation_Add_inv; eauto using Add_head.
Qed.

Theorem Permutation_cons_app_inv l l1 l2 a :
 Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2).A:Type
l, l1, l2:list A
a:A
Permutation (a :: l) (l1 ++ a :: l2) ->
Permutation l (l1 ++ l2)
Proof.A:Type
l, l1, l2:list A
a:A
Permutation (a :: l) (l1 ++ a :: l2) ->
Permutation l (l1 ++ l2)
  intro.A:Type
l, l1, l2:list A
a:A
H:Permutation (a :: l) (l1 ++ a :: l2)
Permutation l (l1 ++ l2) eapply Permutation_Add_inv; eauto using Add_head, Add_app.
Qed.

Theorem Permutation_app_inv_l : forall l l1 l2,
 Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2.A:Type
forall l l1 l2 : list A,
Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2
Proof.A:Type
forall l l1 l2 : list A,
Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2
  induction l; simpl; auto.A:Type
a:A
l:list A
IHl:forall l1 l2 : list A, Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2
forall l1 l2 : list A,
Permutation (a :: l ++ l1) (a :: l ++ l2) ->
Permutation l1 l2
  intros.A:Type
a:A
l:list A
IHl:forall l0 l3 : list A, Permutation (l ++ l0) (l ++ l3) -> Permutation l0 l3
l1, l2:list A
H:Permutation (a :: l ++ l1) (a :: l ++ l2)
Permutation l1 l2
  apply IHl.A:Type
a:A
l:list A
IHl:forall l0 l3 : list A, Permutation (l ++ l0) (l ++ l3) -> Permutation l0 l3
l1, l2:list A
H:Permutation (a :: l ++ l1) (a :: l ++ l2)
Permutation (l ++ l1) (l ++ l2)
  apply Permutation_cons_inv with a; auto.
Qed.

Theorem Permutation_app_inv_r l l1 l2 :
 Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2.A:Type
l, l1, l2:list A
Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2
Proof.A:Type
l, l1, l2:list A
Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2
 rewrite 2 (Permutation_app_comm _ l).A:Type
l, l1, l2:list A
Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2 apply Permutation_app_inv_l.
Qed.

Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a].A:Type
forall (a : A) (l : list A),
Permutation [a] l -> l = [a]
Proof.A:Type
forall (a : A) (l : list A),
Permutation [a] l -> l = [a]
  intros a l H; remember [a] as m in H.A:Type
a:A
l, m:list A
Heqm:m = [a]
H:Permutation m l
l = [a]
  induction H; try (injection Heqm as -> ->);
    discriminate || auto.A:Type
a:A
l':list A
IHPermutation:[] = [a] -> l' = [a]
H:Permutation [] l'
a :: l' = [a]
  apply Permutation_nil in H as ->; trivial.
Qed.

Lemma Permutation_length_1: forall a b, Permutation [a] [b] -> a = b.A:Type
forall a b : A, Permutation [a] [b] -> a = b
Proof.A:Type
forall a b : A, Permutation [a] [b] -> a = b
  intros a b H.A:Type
a, b:A
H:Permutation [a] [b]
a = b
  apply Permutation_length_1_inv in H; injection H as ->; trivial.
Qed.

Lemma Permutation_length_2_inv :
  forall a1 a2 l, Permutation [a1;a2] l -> l = [a1;a2] \/ l = [a2;a1].A:Type
forall (a1 a2 : A) (l : list A),
Permutation [a1; a2] l -> l = [a1; a2] \/ l = [a2; a1]
Proof.A:Type
forall (a1 a2 : A) (l : list A),
Permutation [a1; a2] l -> l = [a1; a2] \/ l = [a2; a1]
  intros a1 a2 l H; remember [a1;a2] as m in H.A:Type
a1, a2:A
l, m:list A
Heqm:m = [a1; a2]
H:Permutation m l
l = [a1; a2] \/ l = [a2; a1]
  revert a1 a2 Heqm.A:Type
l, m:list A
H:Permutation m l
forall a1 a2 : A,
m = [a1; a2] -> l = [a1; a2] \/ l = [a2; a1]
  induction H; intros; try (injection Heqm as ? ?; subst);
    discriminate || (try tauto).A:Type
l':list A
a2:A
IHPermutation:forall a0 a3 : A,
[a2] = [a0; a3] ->
l' = [a0; a3] \/ l' = [a3; a0]
H:Permutation [a2] l'
a1:A
a1 :: l' = [a1; a2] \/ a1 :: l' = [a2; a1]
A:Type
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:forall a0 a3 : A,
l = [a0; a3] ->
l' = [a0; a3] \/ l' = [a3; a0]
IHPermutation2:forall a0 a3 : A,
l' = [a0; a3] ->
l'' = [a0; a3] \/ l'' = [a3; a0]
a1, a2:A
Heqm:l = [a1; a2]
l'' = [a1; a2] \/ l'' = [a2; a1]
  apply Permutation_length_1_inv in H as ->; left; auto.A:Type
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:forall a0 a3 : A,
l = [a0; a3] ->
l' = [a0; a3] \/ l' = [a3; a0]
IHPermutation2:forall a0 a3 : A,
l' = [a0; a3] ->
l'' = [a0; a3] \/ l'' = [a3; a0]
a1, a2:A
Heqm:l = [a1; a2]
l'' = [a1; a2] \/ l'' = [a2; a1]
  apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as [];
    auto.
Qed.

Lemma Permutation_length_2 :
  forall a1 a2 b1 b2, Permutation [a1;a2] [b1;b2] ->
    a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1.A:Type
forall a1 a2 b1 b2 : A,
Permutation [a1; a2] [b1; b2] ->
a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1
Proof.A:Type
forall a1 a2 b1 b2 : A,
Permutation [a1; a2] [b1; b2] ->
a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1
  intros a1 b1 a2 b2 H.A:Type
a1, b1, a2, b2:A
H:Permutation [a1; b1] [a2; b2]
a1 = a2 /\ b1 = b2 \/ a1 = b2 /\ b1 = a2
  apply Permutation_length_2_inv in H as [H|H]; injection H as -> ->; auto.
Qed.

Lemma NoDup_Permutation l l' : NoDup l -> NoDup l' ->
  (forall x:A, In x l <-> In x l') -> Permutation l l'.A:Type
l, l':list A
NoDup l ->
NoDup l' ->
(forall x : A, In x l <-> In x l') -> Permutation l l'
Proof.A:Type
l, l':list A
NoDup l ->
NoDup l' ->
(forall x : A, In x l <-> In x l') -> Permutation l l'
 intros N.A:Type
l, l':list A
N:NoDup l
NoDup l' ->
(forall x : A, In x l <-> In x l') -> Permutation l l' revert l'.A:Type
l:list A
N:NoDup l
forall l' : list A,
NoDup l' ->
(forall x : A, In x l <-> In x l') -> Permutation l l' induction N as [|a l Hal Hl IH].A:Type
forall l' : list A,
NoDup l' ->
(forall x : A, In x [] <-> In x l') ->
Permutation [] l'
A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
IH:forall l' : list A,
NoDup l' ->
(forall x : A, In x l <-> In x l') ->
Permutation l l'
forall l' : list A,
NoDup l' ->
(forall x : A, In x (a :: l) <-> In x l') ->
Permutation (a :: l) l'
 -A:Type
forall l' : list A,
NoDup l' ->
(forall x : A, In x [] <-> In x l') ->
Permutation [] l' destruct l'; simpl; auto.A:Type
a:A
l':list A
NoDup (a :: l') ->
(forall x : A, False <-> a = x \/ In x l') ->
Permutation [] (a :: l')
   intros Hl' H.A:Type
a:A
l':list A
Hl':NoDup (a :: l')
H:forall x : A, False <-> a = x \/ In x l'
Permutation [] (a :: l') exfalso.A:Type
a:A
l':list A
Hl':NoDup (a :: l')
H:forall x : A, False <-> a = x \/ In x l'
False rewrite (H a); auto.
 -A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
IH:forall l' : list A,
NoDup l' ->
(forall x : A, In x l <-> In x l') ->
Permutation l l'
forall l' : list A,
NoDup l' ->
(forall x : A, In x (a :: l) <-> In x l') ->
Permutation (a :: l) l' intros l' Hl' H.A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
IH:forall l'0 : list A,
NoDup l'0 ->
(forall x : A, In x l <-> In x l'0) ->
Permutation l l'0
l':list A
Hl':NoDup l'
H:forall x : A, In x (a :: l) <-> In x l'
Permutation (a :: l) l'
   assert (Ha : In a l') by (apply H; simpl; auto).A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
IH:forall l'0 : list A,
NoDup l'0 ->
(forall x : A, In x l <-> In x l'0) ->
Permutation l l'0
l':list A
Hl':NoDup l'
H:forall x : A, In x (a :: l) <-> In x l'
Ha:In a l'
Permutation (a :: l) l'
   destruct (Add_inv _ _ Ha) as (l'' & AD).A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
IH:forall l'0 : list A,
NoDup l'0 ->
(forall x : A, In x l <-> In x l'0) ->
Permutation l l'0
l':list A
Hl':NoDup l'
H:forall x : A, In x (a :: l) <-> In x l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
Permutation (a :: l) l'
   rewrite <- (Permutation_Add AD).A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
IH:forall l'0 : list A,
NoDup l'0 ->
(forall x : A, In x l <-> In x l'0) ->
Permutation l l'0
l':list A
Hl':NoDup l'
H:forall x : A, In x (a :: l) <-> In x l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
Permutation (a :: l) (a :: l'')
   apply perm_skip.A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
IH:forall l'0 : list A,
NoDup l'0 ->
(forall x : A, In x l <-> In x l'0) ->
Permutation l l'0
l':list A
Hl':NoDup l'
H:forall x : A, In x (a :: l) <-> In x l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
Permutation l l''
   apply IH; clear IH.A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x : A, In x (a :: l) <-> In x l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
NoDup l''
A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x : A, In x (a :: l) <-> In x l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
forall x : A, In x l <-> In x l''
   *A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x : A, In x (a :: l) <-> In x l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
NoDup l'' now apply (NoDup_Add AD).
   *A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x : A, In x (a :: l) <-> In x l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
forall x : A, In x l <-> In x l'' split.A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x0 : A, In x0 (a :: l) <-> In x0 l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
x:A
In x l -> In x l''
A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x0 : A, In x0 (a :: l) <-> In x0 l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
x:A
In x l'' -> In x l
     +A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x0 : A, In x0 (a :: l) <-> In x0 l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
x:A
In x l -> In x l'' apply incl_Add_inv with a l'; trivial.A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x0 : A, In x0 (a :: l) <-> In x0 l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
x:A
incl (a :: l) l' intro.A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x0 : A, In x0 (a :: l) <-> In x0 l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
x, a0:A
In a0 (a :: l) -> In a0 l' apply H.
     +A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x0 : A, In x0 (a :: l) <-> In x0 l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
x:A
In x l'' -> In x l intro Hx.A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x0 : A, In x0 (a :: l) <-> In x0 l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
x:A
Hx:In x l''
In x l
       assert (Hx' : In x (a::l)).A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x0 : A, In x0 (a :: l) <-> In x0 l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
x:A
Hx:In x l''
In x (a :: l)
A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x0 : A, In x0 (a :: l) <-> In x0 l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
x:A
Hx:In x l''
Hx':In x (a :: l)
In x l
       {A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x0 : A, In x0 (a :: l) <-> In x0 l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
x:A
Hx:In x l''
In x (a :: l) apply H.A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x0 : A, In x0 (a :: l) <-> In x0 l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
x:A
Hx:In x l''
In x l' rewrite (Add_in AD).A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x0 : A, In x0 (a :: l) <-> In x0 l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
x:A
Hx:In x l''
In x (a :: l'') now right. }A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x0 : A, In x0 (a :: l) <-> In x0 l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
x:A
Hx:In x l''
Hx':In x (a :: l)
In x l
       destruct Hx'; simpl; trivial.A:Type
a:A
l:list A
Hal:~ In a l
Hl:NoDup l
l':list A
Hl':NoDup l'
H:forall x0 : A, In x0 (a :: l) <-> In x0 l'
Ha:In a l'
l'':list A
AD:Add a l'' l'
x:A
Hx:In x l''
H0:a = x
In x l subst.A:Type
l:list A
x:A
Hal:~ In x l
Hl:NoDup l
l':list A
Hl':NoDup l'
Ha:In x l'
H:forall x0 : A, In x0 (x :: l) <-> In x0 l'
l'':list A
AD:Add x l'' l'
Hx:In x l''
In x l
       rewrite (NoDup_Add AD) in Hl'.A:Type
l:list A
x:A
Hal:~ In x l
Hl:NoDup l
l':list A
Ha:In x l'
H:forall x0 : A, In x0 (x :: l) <-> In x0 l'
l'':list A
Hl':NoDup l'' /\ ~ In x l''
AD:Add x l'' l'
Hx:In x l''
In x l tauto.
Qed.

Lemma NoDup_Permutation_bis l l' : NoDup l -> NoDup l' ->
  length l' <= length l -> incl l l' -> Permutation l l'.A:Type
l, l':list A
NoDup l ->
NoDup l' ->
length l' <= length l -> incl l l' -> Permutation l l'
Proof.A:Type
l, l':list A
NoDup l ->
NoDup l' ->
length l' <= length l -> incl l l' -> Permutation l l'
 intros.A:Type
l, l':list A
H:NoDup l
H0:NoDup l'
H1:length l' <= length l
H2:incl l l'
Permutation l l' apply NoDup_Permutation; auto.A:Type
l, l':list A
H:NoDup l
H0:NoDup l'
H1:length l' <= length l
H2:incl l l'
forall x : A, In x l <-> In x l'
 split; auto.A:Type
l, l':list A
H:NoDup l
H0:NoDup l'
H1:length l' <= length l
H2:incl l l'
x:A
In x l' -> In x l apply NoDup_length_incl; trivial.
Qed.

Lemma Permutation_NoDup l l' : Permutation l l' -> NoDup l -> NoDup l'.A:Type
l, l':list A
Permutation l l' -> NoDup l -> NoDup l'
Proof.A:Type
l, l':list A
Permutation l l' -> NoDup l -> NoDup l'
 induction 1; auto.A:Type
x:A
l, l':list A
H:Permutation l l'
IHPermutation:NoDup l -> NoDup l'
NoDup (x :: l) -> NoDup (x :: l')
A:Type
x, y:A
l:list A
NoDup (y :: x :: l) -> NoDup (x :: y :: l)
 *A:Type
x:A
l, l':list A
H:Permutation l l'
IHPermutation:NoDup l -> NoDup l'
NoDup (x :: l) -> NoDup (x :: l') inversion_clear 1; constructor; eauto using Permutation_in.
 *A:Type
x, y:A
l:list A
NoDup (y :: x :: l) -> NoDup (x :: y :: l) inversion_clear 1 as [|? ? H1 H2].A:Type
x, y:A
l:list A
H1:~ In y (x :: l)
H2:NoDup (x :: l)
NoDup (x :: y :: l) inversion_clear H2; simpl in *.A:Type
x, y:A
l:list A
H1:~ (x = y \/ In y l)
H:~ In x l
H0:NoDup l
NoDup (x :: y :: l)
   constructor.A:Type
x, y:A
l:list A
H1:~ (x = y \/ In y l)
H:~ In x l
H0:NoDup l
~ In x (y :: l)
A:Type
x, y:A
l:list A
H1:~ (x = y \/ In y l)
H:~ In x l
H0:NoDup l
NoDup (y :: l) simpl; intuition.A:Type
x, y:A
l:list A
H1:~ (x = y \/ In y l)
H:~ In x l
H0:NoDup l
NoDup (y :: l) constructor; intuition.
Qed.

Instance Permutation_NoDup' :
 Proper (@Permutation A ==> iff) (@NoDup A) | 10.A:Type
Proper (Permutation (A:=A) ==> iff) (NoDup (A:=A))
Proof.A:Type
Proper (Permutation (A:=A) ==> iff) (NoDup (A:=A))
  repeat red; eauto using Permutation_NoDup.
Qed.

End Permutation_properties.

Section Permutation_map.

Variable A B : Type.
Variable f : A -> B.

Lemma Permutation_map l l' :
  Permutation l l' -> Permutation (map f l) (map f l').A, B:Type
f:A -> B
l, l':list A
Permutation l l' -> Permutation (map f l) (map f l')
Proof.A, B:Type
f:A -> B
l, l':list A
Permutation l l' -> Permutation (map f l) (map f l')
 induction 1; simpl; eauto.
Qed.

Instance Permutation_map' :
  Proper (@Permutation A ==> @Permutation B) (map f) | 10.A, B:Type
f:A -> B
Proper (Permutation (A:=A) ==> Permutation (A:=B))
  (map f)
Proof.A, B:Type
f:A -> B
Proper (Permutation (A:=A) ==> Permutation (A:=B))
  (map f)
  exact Permutation_map.
Qed.

End Permutation_map.

Lemma nat_bijection_Permutation n f :
 bFun n f ->
 Injective f ->
 let l := seq 0 n in Permutation (map f l) l.n:nat
f:nat -> nat
bFun n f ->
Injective f ->
let l := seq 0 n in Permutation (map f l) l
Proof.n:nat
f:nat -> nat
bFun n f ->
Injective f ->
let l := seq 0 n in Permutation (map f l) l
 intros Hf BD.n:nat
f:nat -> nat
Hf:bFun n f
BD:Injective f
let l := seq 0 n in Permutation (map f l) l
 apply NoDup_Permutation_bis; auto using Injective_map_NoDup, seq_NoDup.n:nat
f:nat -> nat
Hf:bFun n f
BD:Injective f
length (seq 0 n) <= length (map f (seq 0 n))
n:nat
f:nat -> nat
Hf:bFun n f
BD:Injective f
incl (map f (seq 0 n)) (seq 0 n)
 *n:nat
f:nat -> nat
Hf:bFun n f
BD:Injective f
length (seq 0 n) <= length (map f (seq 0 n)) now rewrite map_length.
 *n:nat
f:nat -> nat
Hf:bFun n f
BD:Injective f
incl (map f (seq 0 n)) (seq 0 n) intros x.n:nat
f:nat -> nat
Hf:bFun n f
BD:Injective f
x:nat
In x (map f (seq 0 n)) -> In x (seq 0 n) rewrite in_map_iff.n:nat
f:nat -> nat
Hf:bFun n f
BD:Injective f
x:nat
(exists x0 : nat, f x0 = x /\ In x0 (seq 0 n)) ->
In x (seq 0 n) intros (y & <- & Hy').n:nat
f:nat -> nat
Hf:bFun n f
BD:Injective f
y:nat
Hy':In y (seq 0 n)
In (f y) (seq 0 n)
   rewrite in_seq in *.n:nat
f:nat -> nat
Hf:bFun n f
BD:Injective f
y:nat
Hy':0 <= y < 0 + n
0 <= f y < 0 + n simpl in *.n:nat
f:nat -> nat
Hf:bFun n f
BD:Injective f
y:nat
Hy':0 <= y < n
0 <= f y < n
   destruct Hy' as (_,Hy').n:nat
f:nat -> nat
Hf:bFun n f
BD:Injective f
y:nat
Hy':y < n
0 <= f y < n auto with arith.
Qed.

Section Permutation_alt.
Variable A:Type.
Implicit Type a : A.
Implicit Type l : list A.

Alternative characterization of permutation via nth_error and nth

Let adapt f n :=
 let m := f (S n) in if le_lt_dec m (f 0) then m else pred m.

Let adapt_injective f : Injective f -> Injective (adapt f).A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Injective f -> Injective (adapt f)
Proof.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Injective f -> Injective (adapt f)
 unfold adapt.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Injective f ->
Injective
  (fun n : nat =>
   if le_lt_dec (f (S n)) (f 0)
   then f (S n)
   else Nat.pred (f (S n))) intros Hf x y EQ.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
EQ:(if le_lt_dec (f (S x)) (f 0)
 then f (S x)
 else Nat.pred (f (S x))) =
(if le_lt_dec (f (S y)) (f 0)
 then f (S y)
 else Nat.pred (f (S y)))
x = y
 destruct le_lt_dec as [LE|LT]; destruct le_lt_dec as [LE'|LT'].A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LE:f (S x) <= f 0
LE':f (S y) <= f 0
EQ:f (S x) = f (S y)
x = y
A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LE:f (S x) <= f 0
LT':f 0 < f (S y)
EQ:f (S x) = Nat.pred (f (S y))
x = y
A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LT:f 0 < f (S x)
LE':f (S y) <= f 0
EQ:Nat.pred (f (S x)) = f (S y)
x = y
A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LT:f 0 < f (S x)
LT':f 0 < f (S y)
EQ:Nat.pred (f (S x)) = Nat.pred (f (S y))
x = y
 -A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LE:f (S x) <= f 0
LE':f (S y) <= f 0
EQ:f (S x) = f (S y)
x = y now apply eq_add_S, Hf.
 -A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LE:f (S x) <= f 0
LT':f 0 < f (S y)
EQ:f (S x) = Nat.pred (f (S y))
x = y apply Lt.le_lt_or_eq in LE.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LE:f (S x) < f 0 \/ f (S x) = f 0
LT':f 0 < f (S y)
EQ:f (S x) = Nat.pred (f (S y))
x = y
   destruct LE as [LT|EQ']; [|now apply Hf in EQ'].A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LT:f (S x) < f 0
LT':f 0 < f (S y)
EQ:f (S x) = Nat.pred (f (S y))
x = y
   unfold lt in LT.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LT:S (f (S x)) <= f 0
LT':f 0 < f (S y)
EQ:f (S x) = Nat.pred (f (S y))
x = y rewrite EQ in LT.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LT:S (Nat.pred (f (S y))) <= f 0
LT':f 0 < f (S y)
EQ:f (S x) = Nat.pred (f (S y))
x = y
   rewrite <- (Lt.S_pred _ _ LT') in LT.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LT:f (S y) <= f 0
LT':f 0 < f (S y)
EQ:f (S x) = Nat.pred (f (S y))
x = y
   elim (Lt.lt_not_le _ _ LT' LT).
 -A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LT:f 0 < f (S x)
LE':f (S y) <= f 0
EQ:Nat.pred (f (S x)) = f (S y)
x = y apply Lt.le_lt_or_eq in LE'.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LT:f 0 < f (S x)
LE':f (S y) < f 0 \/ f (S y) = f 0
EQ:Nat.pred (f (S x)) = f (S y)
x = y
   destruct LE' as [LT'|EQ']; [|now apply Hf in EQ'].A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LT:f 0 < f (S x)
LT':f (S y) < f 0
EQ:Nat.pred (f (S x)) = f (S y)
x = y
   unfold lt in LT'.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LT:f 0 < f (S x)
LT':S (f (S y)) <= f 0
EQ:Nat.pred (f (S x)) = f (S y)
x = y rewrite <- EQ in LT'.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LT:f 0 < f (S x)
LT':S (Nat.pred (f (S x))) <= f 0
EQ:Nat.pred (f (S x)) = f (S y)
x = y
   rewrite <- (Lt.S_pred _ _ LT) in LT'.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LT:f 0 < f (S x)
LT':f (S x) <= f 0
EQ:Nat.pred (f (S x)) = f (S y)
x = y
   elim (Lt.lt_not_le _ _ LT LT').
 -A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LT:f 0 < f (S x)
LT':f 0 < f (S y)
EQ:Nat.pred (f (S x)) = Nat.pred (f (S y))
x = y apply eq_add_S, Hf.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
f:nat -> nat
Hf:Injective f
x, y:nat
LT:f 0 < f (S x)
LT':f 0 < f (S y)
EQ:Nat.pred (f (S x)) = Nat.pred (f (S y))
f (S x) = f (S y)
   now rewrite (Lt.S_pred _ _ LT), (Lt.S_pred _ _ LT'), EQ.
Qed.

Let adapt_ok a l1 l2 f : Injective f -> length l1 = f 0 ->
 forall n, nth_error (l1++a::l2) (f (S n)) = nth_error (l1++l2) (adapt f n).A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
a:A
l1, l2:list A
f:nat -> nat
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
Proof.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
a:A
l1, l2:list A
f:nat -> nat
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
 unfold adapt.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
a:A
l1, l2:list A
f:nat -> nat
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2)
  (if le_lt_dec (f (S n)) (f 0)
   then f (S n)
   else Nat.pred (f (S n))) intros Hf E n.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
a:A
l1, l2:list A
f:nat -> nat
Hf:Injective f
E:length l1 = f 0
n:nat
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2)
  (if le_lt_dec (f (S n)) (f 0)
   then f (S n)
   else Nat.pred (f (S n)))
 destruct le_lt_dec as [LE|LT].A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
a:A
l1, l2:list A
f:nat -> nat
Hf:Injective f
E:length l1 = f 0
n:nat
LE:f (S n) <= f 0
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (f (S n))
A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
a:A
l1, l2:list A
f:nat -> nat
Hf:Injective f
E:length l1 = f 0
n:nat
LT:f 0 < f (S n)
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (Nat.pred (f (S n)))
 -A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
a:A
l1, l2:list A
f:nat -> nat
Hf:Injective f
E:length l1 = f 0
n:nat
LE:f (S n) <= f 0
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (f (S n)) apply Lt.le_lt_or_eq in LE.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
a:A
l1, l2:list A
f:nat -> nat
Hf:Injective f
E:length l1 = f 0
n:nat
LE:f (S n) < f 0 \/ f (S n) = f 0
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (f (S n))
   destruct LE as [LT|EQ]; [|now apply Hf in EQ].A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
a:A
l1, l2:list A
f:nat -> nat
Hf:Injective f
E:length l1 = f 0
n:nat
LT:f (S n) < f 0
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (f (S n))
   rewrite <- E in LT.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
a:A
l1, l2:list A
f:nat -> nat
Hf:Injective f
E:length l1 = f 0
n:nat
LT:f (S n) < length l1
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (f (S n))
   rewrite 2 nth_error_app1; auto.
 -A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
a:A
l1, l2:list A
f:nat -> nat
Hf:Injective f
E:length l1 = f 0
n:nat
LT:f 0 < f (S n)
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (Nat.pred (f (S n))) rewrite (Lt.S_pred _ _ LT) at 1.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
a:A
l1, l2:list A
f:nat -> nat
Hf:Injective f
E:length l1 = f 0
n:nat
LT:f 0 < f (S n)
nth_error (l1 ++ a :: l2) (S (Nat.pred (f (S n)))) =
nth_error (l1 ++ l2) (Nat.pred (f (S n)))
   rewrite <- E, (Lt.S_pred _ _ LT) in LT.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
a:A
l1, l2:list A
f:nat -> nat
Hf:Injective f
E:length l1 = f 0
n:nat
LT:length l1 < S (Nat.pred (f (S n)))
nth_error (l1 ++ a :: l2) (S (Nat.pred (f (S n)))) =
nth_error (l1 ++ l2) (Nat.pred (f (S n)))
   rewrite 2 nth_error_app2; auto with arith.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
a:A
l1, l2:list A
f:nat -> nat
Hf:Injective f
E:length l1 = f 0
n:nat
LT:length l1 < S (Nat.pred (f (S n)))
nth_error (a :: l2)
  (S (Nat.pred (f (S n))) - length l1) =
nth_error l2 (Nat.pred (f (S n)) - length l1)
   rewrite <- Minus.minus_Sn_m; auto with arith.
Qed.

Lemma Permutation_nth_error l l' :
 Permutation l l' <->
  (length l = length l' /\
   exists f:nat->nat,
    Injective f /\ forall n, nth_error l' n = nth_error l (f n)).A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
Permutation l l' <->
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error l' n = nth_error l (f n)))
Proof.A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
Permutation l l' <->
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error l' n = nth_error l (f n)))
 split.A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
Permutation l l' ->
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error l' n = nth_error l (f n)))
A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error l' n = nth_error l (f n))) ->
Permutation l l'
 {A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
Permutation l l' ->
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error l' n = nth_error l (f n))) intros P.A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
P:Permutation l l'
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error l' n = nth_error l (f n)))
   split; [now apply Permutation_length|].A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
P:Permutation l l'
exists f : nat -> nat,
  Injective f /\
  (forall n : nat, nth_error l' n = nth_error l (f n))
   induction P.A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
exists f : nat -> nat,
  Injective f /\
  (forall n : nat, nth_error [] n = nth_error [] (f n))
A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
x:A
l, l':list A
P:Permutation l l'
IHP:exists f : nat -> nat,
  Injective f /\
  (forall n : nat,
   nth_error l' n = nth_error l (f n))
exists f : nat -> nat,
  Injective f /\
  (forall n : nat,
   nth_error (x :: l') n = nth_error (x :: l) (f n))
A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
x, y:A
l:list A
exists f : nat -> nat,
  Injective f /\
  (forall n : nat,
   nth_error (x :: y :: l) n =
   nth_error (y :: x :: l) (f n))
A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l', l'':list A
P1:Permutation l l'
P2:Permutation l' l''
IHP1:exists f : nat -> nat,
  Injective f /\
  (forall n : nat,
   nth_error l' n = nth_error l (f n))
IHP2:exists f : nat -> nat,
  Injective f /\
  (forall n : nat,
   nth_error l'' n = nth_error l' (f n))
exists f : nat -> nat,
  Injective f /\
  (forall n : nat, nth_error l'' n = nth_error l (f n))
   -A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
exists f : nat -> nat,
  Injective f /\
  (forall n : nat, nth_error [] n = nth_error [] (f n)) exists (fun n => n).A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
Injective (fun n : nat => n) /\
(forall n : nat, nth_error [] n = nth_error [] n)
     split; try red; auto.
   -A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
x:A
l, l':list A
P:Permutation l l'
IHP:exists f : nat -> nat,
  Injective f /\
  (forall n : nat,
   nth_error l' n = nth_error l (f n))
exists f : nat -> nat,
  Injective f /\
  (forall n : nat,
   nth_error (x :: l') n = nth_error (x :: l) (f n)) destruct IHP as (f & Hf & Hf').A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
x:A
l, l':list A
P:Permutation l l'
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
exists f0 : nat -> nat,
  Injective f0 /\
  (forall n : nat,
   nth_error (x :: l') n = nth_error (x :: l) (f0 n))
     exists (fun n => match n with O => O | S n => S (f n) end).A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
x:A
l, l':list A
P:Permutation l l'
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
Injective
  (fun n : nat =>
   match n with
   | 0 => 0
   | S n0 => S (f n0)
   end) /\
(forall n : nat,
 nth_error (x :: l') n =
 nth_error (x :: l)
   match n with
   | 0 => 0
   | S n0 => S (f n0)
   end)
     split; try red.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
x:A
l, l':list A
P:Permutation l l'
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
forall x0 y : nat,
match x0 with
| 0 => 0
| S n => S (f n)
end = match y with
      | 0 => 0
      | S n => S (f n)
      end -> x0 = y
A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
x:A
l, l':list A
P:Permutation l l'
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
forall n : nat,
nth_error (x :: l') n =
nth_error (x :: l)
  match n with
  | 0 => 0
  | S n0 => S (f n0)
  end
     *A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
x:A
l, l':list A
P:Permutation l l'
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
forall x0 y : nat,
match x0 with
| 0 => 0
| S n => S (f n)
end = match y with
      | 0 => 0
      | S n => S (f n)
      end -> x0 = y intros [|y] [|z]; simpl; now auto.
     *A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
x:A
l, l':list A
P:Permutation l l'
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
forall n : nat,
nth_error (x :: l') n =
nth_error (x :: l)
  match n with
  | 0 => 0
  | S n0 => S (f n0)
  end intros [|n]; simpl; auto.
   -A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
x, y:A
l:list A
exists f : nat -> nat,
  Injective f /\
  (forall n : nat,
   nth_error (x :: y :: l) n =
   nth_error (y :: x :: l) (f n)) exists (fun n => match n with 0 => 1 | 1 => 0 | n => n end).A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
x, y:A
l:list A
Injective
  (fun n : nat =>
   match n with
   | 0 => 1
   | 1 => 0
   | S (S _) => n
   end) /\
(forall n : nat,
 nth_error (x :: y :: l) n =
 nth_error (y :: x :: l)
   match n with
   | 0 => 1
   | 1 => 0
   | S (S _) => n
   end)
     split; try red.A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
x, y:A
l:list A
forall x0 y0 : nat,
match x0 with
| 0 => 1
| 1 => 0
| S (S _) => x0
end =
match y0 with
| 0 => 1
| 1 => 0
| S (S _) => y0
end -> x0 = y0
A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
x, y:A
l:list A
forall n : nat,
nth_error (x :: y :: l) n =
nth_error (y :: x :: l)
  match n with
  | 0 => 1
  | 1 => 0
  | S (S _) => n
  end
     *A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
x, y:A
l:list A
forall x0 y0 : nat,
match x0 with
| 0 => 1
| 1 => 0
| S (S _) => x0
end =
match y0 with
| 0 => 1
| 1 => 0
| S (S _) => y0
end -> x0 = y0 intros [|[|z]] [|[|t]]; simpl; now auto.
     *A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
x, y:A
l:list A
forall n : nat,
nth_error (x :: y :: l) n =
nth_error (y :: x :: l)
  match n with
  | 0 => 1
  | 1 => 0
  | S (S _) => n
  end intros [|[|n]]; simpl; auto.
   -A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l', l'':list A
P1:Permutation l l'
P2:Permutation l' l''
IHP1:exists f : nat -> nat,
  Injective f /\
  (forall n : nat,
   nth_error l' n = nth_error l (f n))
IHP2:exists f : nat -> nat,
  Injective f /\
  (forall n : nat,
   nth_error l'' n = nth_error l' (f n))
exists f : nat -> nat,
  Injective f /\
  (forall n : nat, nth_error l'' n = nth_error l (f n)) destruct IHP1 as (f & Hf & Hf').A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l', l'':list A
P1:Permutation l l'
P2:Permutation l' l''
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
IHP2:exists f0 : nat -> nat,
  Injective f0 /\
  (forall n : nat,
   nth_error l'' n = nth_error l' (f0 n))
exists f0 : nat -> nat,
  Injective f0 /\
  (forall n : nat,
   nth_error l'' n = nth_error l (f0 n))
     destruct IHP2 as (g & Hg & Hg').A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l', l'':list A
P1:Permutation l l'
P2:Permutation l' l''
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
g:nat -> nat
Hg:Injective g
Hg':forall n : nat,
nth_error l'' n = nth_error l' (g n)
exists f0 : nat -> nat,
  Injective f0 /\
  (forall n : nat,
   nth_error l'' n = nth_error l (f0 n))
     exists (fun n => f (g n)).A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l', l'':list A
P1:Permutation l l'
P2:Permutation l' l''
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
g:nat -> nat
Hg:Injective g
Hg':forall n : nat,
nth_error l'' n = nth_error l' (g n)
Injective (fun n : nat => f (g n)) /\
(forall n : nat,
 nth_error l'' n = nth_error l (f (g n)))
     split; try red.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l', l'':list A
P1:Permutation l l'
P2:Permutation l' l''
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
g:nat -> nat
Hg:Injective g
Hg':forall n : nat,
nth_error l'' n = nth_error l' (g n)
forall x y : nat, f (g x) = f (g y) -> x = y
A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l', l'':list A
P1:Permutation l l'
P2:Permutation l' l''
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
g:nat -> nat
Hg:Injective g
Hg':forall n : nat,
nth_error l'' n = nth_error l' (g n)
forall n : nat,
nth_error l'' n = nth_error l (f (g n))
     *A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l', l'':list A
P1:Permutation l l'
P2:Permutation l' l''
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
g:nat -> nat
Hg:Injective g
Hg':forall n : nat,
nth_error l'' n = nth_error l' (g n)
forall x y : nat, f (g x) = f (g y) -> x = y auto.
     *A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l', l'':list A
P1:Permutation l l'
P2:Permutation l' l''
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
g:nat -> nat
Hg:Injective g
Hg':forall n : nat,
nth_error l'' n = nth_error l' (g n)
forall n : nat,
nth_error l'' n = nth_error l (f (g n)) intros n.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l', l'':list A
P1:Permutation l l'
P2:Permutation l' l''
f:nat -> nat
Hf:Injective f
Hf':forall n0 : nat,
nth_error l' n0 = nth_error l (f n0)
g:nat -> nat
Hg:Injective g
Hg':forall n0 : nat,
nth_error l'' n0 = nth_error l' (g n0)
n:nat
nth_error l'' n = nth_error l (f (g n)) rewrite <- Hf'; auto. }A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error l' n = nth_error l (f n))) ->
Permutation l l'
 {A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error l' n = nth_error l (f n))) ->
Permutation l l' revert l.A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l':list A
forall l : list A,
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error l' n = nth_error l (f n))) ->
Permutation l l' induction l'.A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
forall l : list A,
length l = length [] /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error [] n = nth_error l (f n))) ->
Permutation l []
A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a0 : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a0 :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
a:A
l':list A
IHl':forall l : list A,
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat,
    nth_error l' n = nth_error l (f n))) ->
Permutation l l'
forall l : list A,
length l = length (a :: l') /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat,
    nth_error (a :: l') n = nth_error l (f n))) ->
Permutation l (a :: l')
   -A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
forall l : list A,
length l = length [] /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error [] n = nth_error l (f n))) ->
Permutation l [] intros [|l] (E & _); now auto.
   -A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a0 : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a0 :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
a:A
l':list A
IHl':forall l : list A,
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat,
    nth_error l' n = nth_error l (f n))) ->
Permutation l l'
forall l : list A,
length l = length (a :: l') /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat,
    nth_error (a :: l') n = nth_error l (f n))) ->
Permutation l (a :: l') intros l (E & f & Hf & Hf').A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a0 :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
E:length l = length (a :: l')
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Permutation l (a :: l')
     simpl in E.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a0 :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
E:length l = S (length l')
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Permutation l (a :: l')
     assert (Ha : nth_error l (f 0) = Some a)
      by (symmetry; apply (Hf' 0)).A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a0 :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
E:length l = S (length l')
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
Permutation l (a :: l')
     destruct (nth_error_split l (f 0) Ha) as (l1 & l2 & L12 & L1).A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n)) =
nth_error (l0 ++ l3) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
E:length l = S (length l')
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
Permutation l (a :: l')
     rewrite L12.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n)) =
nth_error (l0 ++ l3) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
E:length l = S (length l')
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
Permutation (l1 ++ a :: l2) (a :: l') rewrite <- Permutation_middle.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n)) =
nth_error (l0 ++ l3) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
E:length l = S (length l')
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
Permutation (a :: l1 ++ l2) (a :: l') constructor.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n)) =
nth_error (l0 ++ l3) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
E:length l = S (length l')
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
Permutation (l1 ++ l2) l'
     apply IHl'; split; [|exists (adapt f); split].A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n)) =
nth_error (l0 ++ l3) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
E:length l = S (length l')
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
length (l1 ++ l2) = length l'
A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n)) =
nth_error (l0 ++ l3) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
E:length l = S (length l')
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
Injective (adapt f)
A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n)) =
nth_error (l0 ++ l3) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
E:length l = S (length l')
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
forall n : nat,
nth_error l' n = nth_error (l1 ++ l2) (adapt f n)
     *A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n)) =
nth_error (l0 ++ l3) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
E:length l = S (length l')
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
length (l1 ++ l2) = length l' revert E.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n)) =
nth_error (l0 ++ l3) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
length l = S (length l') ->
length (l1 ++ l2) = length l' rewrite L12, !app_length.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n)) =
nth_error (l0 ++ l3) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
length l1 + length (a :: l2) = S (length l') ->
length l1 + length l2 = length l' simpl.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n)) =
nth_error (l0 ++ l3) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
length l1 + S (length l2) = S (length l') ->
length l1 + length l2 = length l'
       rewrite <- plus_n_Sm.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n)) =
nth_error (l0 ++ l3) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
S (length l1 + length l2) = S (length l') ->
length l1 + length l2 = length l' now injection 1.
     *A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n)) =
nth_error (l0 ++ l3) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
E:length l = S (length l')
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
Injective (adapt f) now apply adapt_injective.
     *A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n)) =
nth_error (l0 ++ l3) (adapt f0 n)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l0 (f0 n))) ->
Permutation l0 l'
l:list A
E:length l = S (length l')
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error (a :: l') n = nth_error l (f n)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
forall n : nat,
nth_error l' n = nth_error (l1 ++ l2) (adapt f n) intro n.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n0 : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n0)) =
nth_error (l0 ++ l3) (adapt f0 n0)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n0 : nat,
    nth_error l' n0 = nth_error l0 (f0 n0))) ->
Permutation l0 l'
l:list A
E:length l = S (length l')
f:nat -> nat
Hf:Injective f
Hf':forall n0 : nat,
nth_error (a :: l') n0 = nth_error l (f n0)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
n:nat
nth_error l' n = nth_error (l1 ++ l2) (adapt f n) rewrite <- (adapt_ok a), <- L12; auto.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a0 : A) (l0 l3 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l0 = f0 0 ->
forall n0 : nat,
nth_error (l0 ++ a0 :: l3) (f0 (S n0)) =
nth_error (l0 ++ l3) (adapt f0 n0)
a:A
l':list A
IHl':forall l0 : list A,
length l0 = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n0 : nat,
    nth_error l' n0 = nth_error l0 (f0 n0))) ->
Permutation l0 l'
l:list A
E:length l = S (length l')
f:nat -> nat
Hf:Injective f
Hf':forall n0 : nat,
nth_error (a :: l') n0 = nth_error l (f n0)
Ha:nth_error l (f 0) = Some a
l1, l2:list A
L12:l = l1 ++ a :: l2
L1:length l1 = f 0
n:nat
nth_error l' n = nth_error l (f (S n))
       apply (Hf' (S n)). }
Qed.

Lemma Permutation_nth_error_bis l l' :
 Permutation l l' <->
  exists f:nat->nat,
    Injective f /\
    bFun (length l) f /\
    (forall n, nth_error l' n = nth_error l (f n)).A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
Permutation l l' <->
(exists f : nat -> nat,
   Injective f /\
   bFun (length l) f /\
   (forall n : nat, nth_error l' n = nth_error l (f n)))
Proof.A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
Permutation l l' <->
(exists f : nat -> nat,
   Injective f /\
   bFun (length l) f /\
   (forall n : nat, nth_error l' n = nth_error l (f n)))
 rewrite Permutation_nth_error; split.A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error l' n = nth_error l (f n))) ->
exists f : nat -> nat,
  Injective f /\
  bFun (length l) f /\
  (forall n : nat, nth_error l' n = nth_error l (f n))
A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
(exists f : nat -> nat,
   Injective f /\
   bFun (length l) f /\
   (forall n : nat, nth_error l' n = nth_error l (f n))) ->
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error l' n = nth_error l (f n)))
 -A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error l' n = nth_error l (f n))) ->
exists f : nat -> nat,
  Injective f /\
  bFun (length l) f /\
  (forall n : nat, nth_error l' n = nth_error l (f n)) intros (E & f & Hf & Hf').A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
E:length l = length l'
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
exists f0 : nat -> nat,
  Injective f0 /\
  bFun (length l) f0 /\
  (forall n : nat, nth_error l' n = nth_error l (f0 n))
   exists f.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
E:length l = length l'
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
Injective f /\
bFun (length l) f /\
(forall n : nat, nth_error l' n = nth_error l (f n)) do 2 (split; trivial).A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
E:length l = length l'
f:nat -> nat
Hf:Injective f
Hf':forall n : nat,
nth_error l' n = nth_error l (f n)
bFun (length l) f
   intros n Hn.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
E:length l = length l'
f:nat -> nat
Hf:Injective f
Hf':forall n0 : nat,
nth_error l' n0 = nth_error l (f n0)
n:nat
Hn:n < length l
f n < length l
   destruct (Lt.le_or_lt (length l) (f n)) as [LE|LT]; trivial.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
E:length l = length l'
f:nat -> nat
Hf:Injective f
Hf':forall n0 : nat,
nth_error l' n0 = nth_error l (f n0)
n:nat
Hn:n < length l
LE:length l <= f n
f n < length l
   rewrite <- nth_error_None, <- Hf', nth_error_None, <- E in LE.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
E:length l = length l'
f:nat -> nat
Hf:Injective f
Hf':forall n0 : nat,
nth_error l' n0 = nth_error l (f n0)
n:nat
Hn:n < length l
LE:length l <= n
f n < length l
   elim (Lt.lt_not_le _ _ Hn LE).
 -A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
(exists f : nat -> nat,
   Injective f /\
   bFun (length l) f /\
   (forall n : nat, nth_error l' n = nth_error l (f n))) ->
length l = length l' /\
(exists f : nat -> nat,
   Injective f /\
   (forall n : nat, nth_error l' n = nth_error l (f n))) intros (f & Hf & Hf2 & Hf3); split; [|exists f; auto].A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
length l = length l'
   assert (H : length l' <= length l') by auto with arith.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l' <= length l'
length l = length l'
   rewrite <- nth_error_None, Hf3, nth_error_None in H.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l <= f (length l')
length l = length l'
   destruct (Lt.le_or_lt (length l) (length l')) as [LE|LT];
    [|apply Hf2 in LT; elim (Lt.lt_not_le _ _ LT H)].A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l <= f (length l')
LE:length l <= length l'
length l = length l'
   apply Lt.le_lt_or_eq in LE.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l <= f (length l')
LE:length l < length l' \/ length l = length l'
length l = length l' destruct LE as [LT|EQ]; trivial.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l <= f (length l')
LT:length l < length l'
length l = length l'
   rewrite <- nth_error_Some, Hf3, nth_error_Some in LT.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l <= f (length l')
LT:f (length l) < length l
length l = length l'
   assert (Hf' : bInjective (length l) f).A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l <= f (length l')
LT:f (length l) < length l
bInjective (length l) f
A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l <= f (length l')
LT:f (length l) < length l
Hf':bInjective (length l) f
length l = length l'
   {A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l <= f (length l')
LT:f (length l) < length l
bInjective (length l) f intros x y _ _ E.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l <= f (length l')
LT:f (length l) < length l
x, y:nat
E:f x = f y
x = y now apply Hf. }A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l <= f (length l')
LT:f (length l) < length l
Hf':bInjective (length l) f
length l = length l'
   rewrite (bInjective_bSurjective Hf2) in Hf'.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l <= f (length l')
LT:f (length l) < length l
Hf':bSurjective (length l) f
length l = length l'
   destruct (Hf' _ LT) as (y & Hy & Hy').A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l <= f (length l')
LT:f (length l) < length l
Hf':bSurjective (length l) f
y:nat
Hy:y < length l
Hy':f y = f (length l)
length l = length l'
   apply Hf in Hy'.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l <= f (length l')
LT:f (length l) < length l
Hf':bSurjective (length l) f
y:nat
Hy:y < length l
Hy':y = length l
length l = length l' subst y.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
H:length l <= f (length l')
LT:f (length l) < length l
Hf':bSurjective (length l) f
Hy:length l < length l
length l = length l' elim (Lt.lt_irrefl _ Hy).
Qed.

Lemma Permutation_nth l l' d :
 Permutation l l' <->
  (let n := length l in
   length l' = n /\
   exists f:nat->nat,
    bFun n f /\
    bInjective n f /\
    (forall x, x < n -> nth x l' d = nth (f x) l d)).A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
d:A
Permutation l l' <->
(let n := length l in
 length l' = n /\
 (exists f : nat -> nat,
    bFun n f /\
    bInjective n f /\
    (forall x : nat,
     x < n -> nth x l' d = nth (f x) l d)))
Proof.A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
d:A
Permutation l l' <->
(let n := length l in
 length l' = n /\
 (exists f : nat -> nat,
    bFun n f /\
    bInjective n f /\
    (forall x : nat,
     x < n -> nth x l' d = nth (f x) l d)))
 split.A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
d:A
Permutation l l' ->
let n := length l in
length l' = n /\
(exists f : nat -> nat,
   bFun n f /\
   bInjective n f /\
   (forall x : nat,
    x < n -> nth x l' d = nth (f x) l d))
A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
d:A
(let n := length l in
 length l' = n /\
 (exists f : nat -> nat,
    bFun n f /\
    bInjective n f /\
    (forall x : nat,
     x < n -> nth x l' d = nth (f x) l d))) ->
Permutation l l'
 -A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
d:A
Permutation l l' ->
let n := length l in
length l' = n /\
(exists f : nat -> nat,
   bFun n f /\
   bInjective n f /\
   (forall x : nat,
    x < n -> nth x l' d = nth (f x) l d)) intros H.A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
d:A
H:Permutation l l'
let n := length l in
length l' = n /\
(exists f : nat -> nat,
   bFun n f /\
   bInjective n f /\
   (forall x : nat,
    x < n -> nth x l' d = nth (f x) l d))
   assert (E := Permutation_length H).A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
d:A
H:Permutation l l'
E:length l = length l'
let n := length l in
length l' = n /\
(exists f : nat -> nat,
   bFun n f /\
   bInjective n f /\
   (forall x : nat,
    x < n -> nth x l' d = nth (f x) l d))
   split; auto.A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
d:A
H:Permutation l l'
E:length l = length l'
exists f : nat -> nat,
  bFun (length l) f /\
  bInjective (length l) f /\
  (forall x : nat,
   x < length l -> nth x l' d = nth (f x) l d)
   apply Permutation_nth_error_bis in H.A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
d:A
H:exists f : nat -> nat,
  Injective f /\
  bFun (length l) f /\
  (forall n : nat,
   nth_error l' n = nth_error l (f n))
E:length l = length l'
exists f : nat -> nat,
  bFun (length l) f /\
  bInjective (length l) f /\
  (forall x : nat,
   x < length l -> nth x l' d = nth (f x) l d)
   destruct H as (f & Hf & Hf2 & Hf3).A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
E:length l = length l'
exists f0 : nat -> nat,
  bFun (length l) f0 /\
  bInjective (length l) f0 /\
  (forall x : nat,
   x < length l -> nth x l' d = nth (f0 x) l d)
   exists f.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
E:length l = length l'
bFun (length l) f /\
bInjective (length l) f /\
(forall x : nat,
 x < length l -> nth x l' d = nth (f x) l d) split; [|split]; auto.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
E:length l = length l'
bInjective (length l) f
A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
E:length l = length l'
forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
   intros x y _ _ Hxy.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
E:length l = length l'
x, y:nat
Hxy:f x = f y
x = y
A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
E:length l = length l'
forall x : nat,
x < length l -> nth x l' d = nth (f x) l d now apply Hf.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n : nat,
nth_error l' n = nth_error l (f n)
E:length l = length l'
forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
   intros n Hn.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n0 : nat,
nth_error l' n0 = nth_error l (f n0)
E:length l = length l'
n:nat
Hn:n < length l
nth n l' d = nth (f n) l d rewrite <- 2 nth_default_eq.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n0 : nat,
nth_error l' n0 = nth_error l (f n0)
E:length l = length l'
n:nat
Hn:n < length l
nth_default d l' n = nth_default d l (f n) unfold nth_default.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
f:nat -> nat
Hf:Injective f
Hf2:bFun (length l) f
Hf3:forall n0 : nat,
nth_error l' n0 = nth_error l (f n0)
E:length l = length l'
n:nat
Hn:n < length l
match nth_error l' n with
| Some x => x
| None => d
end =
match nth_error l (f n) with
| Some x => x
| None => d
end
    now rewrite Hf3.
 -A:Type
adapt:=fun (f : nat -> nat) (n : nat) =>
let m := f (S n) in
if le_lt_dec m (f 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f : nat -> nat,
Injective f -> Injective (adapt f)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f : nat -> nat),
Injective f ->
length l1 = f 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f (S n)) =
nth_error (l1 ++ l2) (adapt f n)
l, l':list A
d:A
(let n := length l in
 length l' = n /\
 (exists f : nat -> nat,
    bFun n f /\
    bInjective n f /\
    (forall x : nat,
     x < n -> nth x l' d = nth (f x) l d))) ->
Permutation l l' intros (E & f & Hf1 & Hf2 & Hf3).A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
Permutation l l'
   rewrite Permutation_nth_error.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
length l = length l' /\
(exists f0 : nat -> nat,
   Injective f0 /\
   (forall n : nat,
    nth_error l' n = nth_error l (f0 n)))
   split; auto.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
exists f0 : nat -> nat,
  Injective f0 /\
  (forall n : nat, nth_error l' n = nth_error l (f0 n))
   exists (fun n => if le_lt_dec (length l) n then n else f n).A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
Injective
  (fun n : nat =>
   if le_lt_dec (length l) n then n else f n) /\
(forall n : nat,
 nth_error l' n =
 nth_error l
   (if le_lt_dec (length l) n then n else f n))
   split.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
Injective
  (fun n : nat =>
   if le_lt_dec (length l) n then n else f n)
A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
forall n : nat,
nth_error l' n =
nth_error l
  (if le_lt_dec (length l) n then n else f n)
   *A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
Injective
  (fun n : nat =>
   if le_lt_dec (length l) n then n else f n) intros x y.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x0 : nat,
x0 < length l -> nth x0 l' d = nth (f x0) l d
x, y:nat
(if le_lt_dec (length l) x then x else f x) =
(if le_lt_dec (length l) y then y else f y) -> x = y
     destruct le_lt_dec as [LE|LT];
      destruct le_lt_dec as [LE'|LT']; auto.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x0 : nat,
x0 < length l -> nth x0 l' d = nth (f x0) l d
x, y:nat
LE:length l <= x
LT':y < length l
x = f y -> x = y
A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x0 : nat,
x0 < length l -> nth x0 l' d = nth (f x0) l d
x, y:nat
LT:x < length l
LE':length l <= y
f x = y -> x = y
     +A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x0 : nat,
x0 < length l -> nth x0 l' d = nth (f x0) l d
x, y:nat
LE:length l <= x
LT':y < length l
x = f y -> x = y apply Hf1 in LT'.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x0 : nat,
x0 < length l -> nth x0 l' d = nth (f x0) l d
x, y:nat
LE:length l <= x
LT':f y < length l
x = f y -> x = y intros ->.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
y:nat
LE:length l <= f y
LT':f y < length l
f y = y
       elim (Lt.lt_irrefl (f y)).A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
y:nat
LE:length l <= f y
LT':f y < length l
f y < f y eapply Lt.lt_le_trans; eauto.
     +A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x0 : nat,
x0 < length l -> nth x0 l' d = nth (f x0) l d
x, y:nat
LT:x < length l
LE':length l <= y
f x = y -> x = y apply Hf1 in LT.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x0 : nat,
x0 < length l -> nth x0 l' d = nth (f x0) l d
x, y:nat
LT:f x < length l
LE':length l <= y
f x = y -> x = y intros <-.A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x0 : nat,
x0 < length l -> nth x0 l' d = nth (f x0) l d
x:nat
LT:f x < length l
LE':length l <= f x
x = f x
       elim (Lt.lt_irrefl (f x)).A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x0 : nat,
x0 < length l -> nth x0 l' d = nth (f x0) l d
x:nat
LT:f x < length l
LE':length l <= f x
f x < f x eapply Lt.lt_le_trans; eauto.
   *A:Type
adapt:=fun (f0 : nat -> nat) (n : nat) =>
let m := f0 (S n) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n : nat,
nth_error (l1 ++ a :: l2) (f0 (S n)) =
nth_error (l1 ++ l2) (adapt f0 n)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
forall n : nat,
nth_error l' n =
nth_error l
  (if le_lt_dec (length l) n then n else f n) intros n.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
n:nat
nth_error l' n =
nth_error l
  (if le_lt_dec (length l) n then n else f n)
     destruct le_lt_dec as [LE|LT].A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
n:nat
LE:length l <= n
nth_error l' n = nth_error l n
A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
n:nat
LT:n < length l
nth_error l' n = nth_error l (f n)
     +A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
n:nat
LE:length l <= n
nth_error l' n = nth_error l n assert (LE' : length l' <= n) by (now rewrite E).A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
n:nat
LE:length l <= n
LE':length l' <= n
nth_error l' n = nth_error l n
       rewrite <- nth_error_None in LE, LE'.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
n:nat
LE:nth_error l n = None
LE':nth_error l' n = None
nth_error l' n = nth_error l n congruence.
     +A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
n:nat
LT:n < length l
nth_error l' n = nth_error l (f n) assert (LT' : n < length l') by (now rewrite E).A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
Hf3:forall x : nat,
x < length l -> nth x l' d = nth (f x) l d
n:nat
LT:n < length l
LT':n < length l'
nth_error l' n = nth_error l (f n)
       specialize (Hf3 n LT).A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
n:nat
Hf3:nth n l' d = nth (f n) l d
LT:n < length l
LT':n < length l'
nth_error l' n = nth_error l (f n) rewrite <- 2 nth_default_eq in Hf3.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
n:nat
Hf3:nth_default d l' n = nth_default d l (f n)
LT:n < length l
LT':n < length l'
nth_error l' n = nth_error l (f n)
       unfold nth_default in Hf3.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
n:nat
Hf3:match nth_error l' n with
| Some x => x
| None => d
end =
match nth_error l (f n) with
| Some x => x
| None => d
end
LT:n < length l
LT':n < length l'
nth_error l' n = nth_error l (f n)
       apply Hf1 in LT.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
n:nat
Hf3:match nth_error l' n with
| Some x => x
| None => d
end =
match nth_error l (f n) with
| Some x => x
| None => d
end
LT:f n < length l
LT':n < length l'
nth_error l' n = nth_error l (f n)
       rewrite <- nth_error_Some in LT, LT'.A:Type
adapt:=fun (f0 : nat -> nat) (n0 : nat) =>
let m := f0 (S n0) in
if le_lt_dec m (f0 0) then m else Nat.pred m:(nat -> nat) -> nat -> nat
adapt_injective:forall f0 : nat -> nat,
Injective f0 -> Injective (adapt f0)
adapt_ok:forall (a : A) (l1 l2 : list A)
  (f0 : nat -> nat),
Injective f0 ->
length l1 = f0 0 ->
forall n0 : nat,
nth_error (l1 ++ a :: l2) (f0 (S n0)) =
nth_error (l1 ++ l2) (adapt f0 n0)
l, l':list A
d:A
E:length l' = length l
f:nat -> nat
Hf1:bFun (length l) f
Hf2:bInjective (length l) f
n:nat
Hf3:match nth_error l' n with
| Some x => x
| None => d
end =
match nth_error l (f n) with
| Some x => x
| None => d
end
LT:nth_error l (f n) <> None
LT':nth_error l' n <> None
nth_error l' n = nth_error l (f n)
       do 2 destruct nth_error; congruence.
Qed.

End Permutation_alt.

(* begin hide *)
Notation Permutation_app_swap := Permutation_app_comm (only parsing).
(* end hide *)