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