proposition: Lemma nonZero : forall x : Q, ~(x==0) -> ~(Qmake (Z.sgn (Qnum x) * Qden x)%Z (posZ (Qnum x))==0).
proof: Proof. intro x. unfold Qeq in |- *. unfold Qnum at 2 6 in |- *. repeat rewrite Zmult_0_l. unfold Qden at 1 3 in |- *. repeat rewrite Zplus_0_l. repeat rewrite Zmult_1_r. simpl in |- *. intro H. cut (Z.sgn (Qnum x) <> 0%Z). intro H0. cut (Zpos (Qden x) <> 0%Z). intro H1. intro H2. elim H0. exact (Zmult_integral_l (Qden x) (Z.sgn (Qnum x)) H1 H2). apply Zgt_not_eq. auto with zarith. apply Zsgn_3. intro; elim H; auto. Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q