proposition: Theorem Q_is_denumerable: is_denumerable Q.
proof: Proof. apply is_denumerable_transitive with Z. apply Z_is_denumerable. exists Q_to_Z_i; exists Z_to_Q_i; split; [ apply Q_to_Z_to_Q_i | apply Z_to_Q_to_Z_i ]. Defined.
imports: Coq(ZArith) Coq(Lia) QArithSternBrocot(Q_field)