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