proposition: 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)).
proof: Proof. rewrite Permutation_nth_error; split. - intros (E & f & Hf & Hf'). exists f. do 2 (split; trivial). intros n Hn. destruct (Nat.le_gt_cases (length l) (f n)) as [LE|LT]; trivial. rewrite <- nth_error_None, <- Hf', nth_error_None, <- E in LE. elim (proj1 (Nat.lt_nge _ _) Hn LE). - intros (f & Hf & Hf2 & Hf3); split; [|exists f; auto]. assert (H : length l' <= length l') by auto. rewrite <- nth_error_None, Hf3, nth_error_None in H. destruct (Nat.le_gt_cases (length l) (length l')) as [LE|LT]; [|apply Hf2 in LT; elim (proj1 (Nat.lt_nge _ _) LT H)]. apply Nat.lt_eq_cases in LE. destruct LE as [LT|EQ]; trivial. rewrite <- nth_error_Some, Hf3, nth_error_Some in LT. assert (Hf' : bInjective (length l) f). { intros x y _ _ E. now apply Hf. } rewrite (bInjective_bSurjective Hf2) in Hf'. destruct (Hf' _ LT) as (y & Hy & Hy'). apply Hf in Hy'. subst y. elim (Nat.lt_irrefl _ Hy). Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat