proposition: Lemma FiniteT_nat_no_surj (X : Type) : FiniteT X -> ~ exists f : X -> nat, surjective f.
proof: Proof. intros. induction H. - intro. destruct H. specialize (H O). destruct H. assumption. - intro. destruct H0 as [f]. apply IHFiniteT. clear IHFiniteT. exists (fun x => if (f None) <? f (Some x) then pred (f (Some x)) else f (Some x)). red; intros. destruct (H0 y) as [[|]]. + destruct (f None <? y) eqn:E. * destruct (H0 (S y)) as [[|]]. -- exists t0. subst. rewrite H2. simpl. replace (f None <? S (f (Some t))) with true. { reflexivity. } symmetry. rewrite Nat.ltb_lt. rewrite Nat.ltb_lt in E. apply Nat.lt_lt_succ_r. assumption. -- subst. rewrite H2 in E. rewrite Nat.ltb_lt in E. apply Nat.nlt_succ_diag_l in E. contradiction. * exists t. subst. rewrite E. reflexivity. + destruct (H0 (S y)) as [[|]]. -- exists t. subst. rewrite H2. replace (f None <? S (f None)) with true. { reflexivity. } symmetry. rewrite Nat.ltb_lt. constructor. -- rewrite H1 in H2. apply n_Sn in H2. contradiction. - intro. destruct H1. apply IHFiniteT. exists (compose x f). apply invertible_impl_bijective in H0. destruct H0. apply surjective_compose; assumption. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)