proposition: Lemma Qmult_inject_Z_l : forall (a : Z) (b : positive) (z : Z), (inject_Z z) * (a#b) == z*a#b.
proof: Proof. intros a b z. unfold Qeq. cbn. ring. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool