proposition: Lemma Permutation_map_lt_nil {A f} : (forall n, n < f n) -> Permutation (map f A) A -> A = [].
proof: Proof. move=> Hf /Permutation_sym /(@Permutation_in nat). move: A => [|a A]; first done. move: (a :: A) (in_eq a A) => {}A + HA. elim /(Nat.measure_induction _ id): a. move=> a IH /HA /in_map_iff [b] [?]. subst a. by apply: (IH b (Hf b)). Qed.
imports: ssreflect ssrbool ssrfun PeanoNat Lia Permutation List