proposition: 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)).
proof: Proof. split. - intros H. assert (E := Permutation_length H). split; auto. apply Permutation_nth_error_bis in H. destruct H as (f & Hf & Hf2 & Hf3). exists f. split; [|split]; auto. + intros x y _ _ Hxy. now apply Hf. + intros n Hn. rewrite <- 2 nth_default_eq. unfold nth_default. now rewrite Hf3. - intros (E & f & Hf1 & Hf2 & Hf3). rewrite Permutation_nth_error. split; auto. exists (fun n => if le_lt_dec (length l) n then n else f n). split. * intros x y. destruct le_lt_dec as [LE|LT]; destruct le_lt_dec as [LE'|LT']; auto. + apply Hf1 in LT'. intros ->. elim (Nat.lt_irrefl (f y)). eapply Nat.lt_le_trans; eauto. + apply Hf1 in LT. intros <-. elim (Nat.lt_irrefl (f x)). eapply Nat.lt_le_trans; eauto. * intros n. destruct le_lt_dec as [LE|LT]. + assert (LE' : length l' <= n) by (now rewrite E). rewrite <- nth_error_None in LE, LE'. congruence. + assert (LT' : n < length l') by (now rewrite E). specialize (Hf3 n LT). rewrite <- 2 nth_default_eq in Hf3. unfold nth_default in Hf3. apply Hf1 in LT. rewrite <- nth_error_Some in LT, LT'. do 2 destruct nth_error; congruence. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat