proposition: Lemma Qreduce_r : forall (a : Z) (b z : positive), a*(Zpos z) # b*z == a#b.
proof: Proof. intros a b z. unfold Qeq, Qnum, Qden. rewrite Pos2Z.inj_mul. ring. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool