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