proposition: Lemma bInjective_bSurjective n (f:nat->nat) : bFun n f -> (bInjective n f <-> bSurjective n f).
proof: Proof. intros h. rewrite <- (restrict_injective h), <- (restrict_surjective h). apply Endo_Injective_Surjective. - apply Fin_Finite. - intros x y. destruct (Fin.eq_dec x y); [left|right]; trivial. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec