proposition: Lemma extend_injective n f : bInjective n (@extend n f) <-> Injective f.
proof: Proof. split. - intros hf x y Eq. apply f2n_inj. apply hf; try apply f2n_ok. now rewrite 2 extend_f2n, Eq. - intros hf x y hx hy Eq. rewrite <- (f2n_n2f hx), <- (f2n_n2f hy). f_equal. apply hf. rewrite <- 2 extend_n2f. generalize (extend_ok f hx) (extend_ok f hy). rewrite Eq. apply n2f_ext. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec