proposition: Lemma bSurjective_bBijective n (f:nat->nat) : bFun n f -> bSurjective n f -> exists g, bFun n g /\ forall x, x < n -> g (f x) = x /\ f (g x) = x.
proof: Proof. intro hf. rewrite <- (restrict_surjective hf). intros Su. assert (Ij : Injective (restrict hf)). { apply Endo_Injective_Surjective; trivial. - apply Fin_Finite. - intros x y. destruct (Fin.eq_dec x y); [left|right]; trivial. } assert (Bi : Bijective (restrict hf)). { apply Injective_Surjective_Bijective; trivial. - apply Fin_Finite. - exact Fin.eq_dec. } destruct Bi as (g & Hg & Hg'). exists (extend g). split. - apply extend_ok. - intros x Hx. split. + now rewrite <- (f2n_n2f Hx), <- (restrict_f2n hf), extend_f2n, Hg. + now rewrite <- (f2n_n2f Hx), extend_f2n, <- (restrict_f2n hf), Hg'. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec