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