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