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