proposition: Lemma Q_non_zero : forall x : Q, (x/=0) -> Qnum x <> 0%Z.
proof: Proof. firstorder auto with qarith zarith. Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q