proposition: Lemma finite_nat_initial_segment_ens (n : nat) : Finite (fun m => m < n).
proof: Proof. induction n. { replace (fun _ => _) with (@Empty_set nat). { constructor. } apply Extensionality_Ensembles; split; auto with sets. intros x Hx. red in Hx. inversion Hx. } replace (fun _ => _) with (Add (fun m => m < n) n). { constructor; auto. intros ?. red in H. lia. } clear IHn. apply Extensionality_Ensembles; split; intros m Hm. - inversion Hm; subst; clear Hm. + cbv in *. lia. + inversion H; subst; clear H. constructor. - cbv in *. apply le_S_n in Hm. destruct Hm. + right. constructor. + left. cbv. apply le_n_S. assumption. Qed.
imports: Coq(Classical Lia) ZornsLemma(DecidableDec EnsemblesImplicit Families FiniteImplicit FunctionPropertiesEns Powerset_facts Image InverseImage ReverseMath.AddSubtract)