proposition: Lemma positive_countable: CountableT positive.
proof: Proof. exists nat_of_P. intros n1 n2 ?. now apply nat_of_P_inj. Qed.
imports: FiniteTypes Relation_Definitions ZArith QArith IndexedFamilies InfiniteTypes CSB DecidableDec FunctionalExtensionality ProofIrrelevance DependentTypeChoice ClassicalChoice Arith ArithRing