proposition: Lemma Q_countable: CountableT Q.
proof: Proof. destruct countable_nat_product as [f], positive_countable as [g], Z_countable as [h]. exists (fun q:Q => match q with n # d => f (h n, g d) end)%Q. intros [n1 d1] [n2 d2] ?. apply H in H2. injection H2 as H2. f_equal; auto. Qed.
imports: FiniteTypes Relation_Definitions ZArith QArith IndexedFamilies InfiniteTypes CSB DecidableDec FunctionalExtensionality ProofIrrelevance DependentTypeChoice ClassicalChoice Arith ArithRing