proposition: Lemma finite_nat_initial_segment: forall n:nat, FiniteT { m:nat | m < n }.
proof: Proof. intros. apply Finite_ens_type. apply finite_nat_initial_segment_ens. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)