proposition: Lemma Qnum_cancel : forall (a b : positive) (z : Z), z<>0%Z -> (z#a)==(z#b) -> a=b.
proof: Proof. intros a b z Hz_ne_0. unfold Qeq. rewrite Z.eq_sym_iff, <- Pos2Z.inj_iff. apply (Z.mul_reg_l _ _ _ Hz_ne_0). Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool