proposition: Lemma Qreduce_den_inject_Z_r : forall (a : Z) (b : positive), a * Z.pos b # b == inject_Z a.
proof: Proof. intros a b. unfold Qeq, Qnum, Qden, inject_Z. ring. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool