proposition: Lemma nat_bijection_Permutation n f : bFun n f -> Injective f -> let l := seq 0 n in Permutation (map f l) l.
proof: Proof. intros Hf BD. apply NoDup_Permutation_bis; auto using Injective_map_NoDup, seq_NoDup. * now rewrite map_length. * intros x. rewrite in_map_iff. intros (y & <- & Hy'). rewrite in_seq in *. simpl in *. destruct Hy' as (_,Hy'). split; [ apply Nat.le_0_l | auto ]. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat