proposition: Lemma finite_nat_initial_segment_le (n : nat) : FiniteT { m : nat | (m <= n)%nat }.
proof: Proof. apply Finite_ens_type. replace (fun _ => _) with (fun m => m < S n). { apply finite_nat_initial_segment_ens. } apply Extensionality_Ensembles; split; intros m Hm; cbv in *; lia. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)