proposition: Lemma nat_countable : CountableT nat.
proof: Proof. apply intro_nat_injection with (fun n => n). now intros [|m] [|n]. Qed.
imports: FiniteTypes Relation_Definitions ZArith QArith IndexedFamilies InfiniteTypes CSB DecidableDec FunctionalExtensionality ProofIrrelevance DependentTypeChoice ClassicalChoice Arith ArithRing