proposition: Lemma FiniteT_nat_embeds {X : Type} : FiniteT X -> exists f : X -> nat, injective f.
proof: Proof. intros. induction H. - exists (fun _ => O). red; intros. contradiction. - destruct IHFiniteT as [f]. exists (fun a => match a with | None => O | Some b => S (f b) end). red; intros. destruct x, y; try discriminate. + inversion H1; subst; clear H1. apply H0 in H3. rewrite H3. reflexivity. + reflexivity. - destruct IHFiniteT as [g]. destruct H0 as [f']. exists (fun y => g (f' y)). apply injective_compose. 2: { assumption. } destruct (invertible_impl_bijective f'). 2: { assumption. } exists f; assumption. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)