proposition: Lemma infinite_inj P : (exists f : nat -> elts P, injective f) -> infinite P.
proof: Proof. intros [f f_inj] [n [g [g_inj g_surj]]]. assert (S n <= n). 2: lia. apply N_inj_le with (f := inverse g_surj o f o (@N_val _)). inj. apply inj_N_val. Qed.
imports: Coq(Basics Morphisms Setoid Lia) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil SetUtil FinSet FunUtil BoundNat IotaUtil EpsilonUtil)