proposition: Lemma positive_nonzero_in_Q (p: positive): ~ inject_Z (Zpos p) == 0.
proof: Proof. discriminate. Qed.
imports: Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith Coq.QArith.Qpower Coq.QArith.Qround Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List