proposition: Lemma Qden_cancel : forall (a b : Z) (p : positive), (a#p)==(b#p) -> a=b.
proof: Proof. intros a b p. unfold Qeq. apply Z.mul_cancel_r, not_eq_sym, Z.lt_neq, Pos2Z.is_pos. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool