proposition: Lemma restrict_surjective n f h : Surjective (@restrict n f h) <-> bSurjective n f.
proof: Proof. split. - intros hf y hy. destruct (hf (n2f hy)) as (x,Eq). exists (f2n x). split. + apply f2n_ok. + rewrite <- (restrict_f2n h), Eq. apply f2n_n2f. - intros hf y. destruct (hf _ (f2n_ok y)) as (x & hx & Eq). exists (n2f hx). apply f2n_inj. now rewrite restrict_f2n, f2n_n2f. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec