proposition: Lemma seq_range_countable : forall f, Countable (seq_range f).
proof: Proof. intros f. unfold seq_range. rewrite image_as_Im. apply countable_img. apply countable_type_ensemble. apply nat_countable. Qed.
imports: Coq(Ensembles Arith ArithRing Wellfounded Relations Wf_nat Finite_sets Logic.Epsilon Sets.Image Lia) ZornsLemma(Classical_Wf CountableTypes Families) hydras(MoreEpsilonIota PartialFun GRelations Prelude.More_Arith)