4 proofs suggested for Rational.Properties

[mechvel]

I suggest to add to Data.Rational.Properties the following functions.
This is because they are usable, and their analogues are in Data.Nat.Properties :

≤⇒≯ : {x y : ℚ} → x ≤ y → x ≯ y
≤⇒≯ {x} {y} x≤y y<x =  <⇒≢ y<x y=x
     where
     y≤x = <⇒≤ y<x;   x=y = ≤-antisym x≤y y≤x;   y=x = sym x=y

p*q≡0⇒p≡0∨q≡0 : {p q : ℚ} → p * q ≡ 0ℚ → p ≡ 0ℚ ⊎ q ≡ 0ℚ
p*q≡0⇒p≡0∨q≡0  {x} {y} xy=0
   with <-cmp x 0ℚ | <-cmp y 0ℚ
   ...

p*q≢0⇒p≢0 : {p q : ℚ} → p * q ≢ 0ℚ → p ≢ 0ℚ
...

p*q≢0⇒q≢0 : {p q : ℚ} → p * q ≢ 0ℚ → q ≢ 0ℚ
...

[jamesmckinna]

The first of these can surely be simplified to:

≤⇒≯ : {x y : ℚ} → x ≤ y → x ≯ y
≤⇒≯ {x} {y} x≤y y<x =  <⇒≢ y<x y=x
     where
     y≤x = <⇒≤ y<x; y=x = ≤-antisym y≤x x≤y

and hence even inlined simply as:

≤⇒≯ : {x y : ℚ} → x ≤ y → x ≯ y
≤⇒≯ {x} {y} x≤y y<x =  <⇒≢ y<x (≤-antisym (<⇒≤ y<x) x≤y)

But the pattern of the rest of the Relational properties section of Data.Rational.Properties is precisely to delegate the proofs of such lemmas to the corresponding ones for ℤ... is that possible in this instance? UPDATED: yes

≤⇒≯ : _≤_ ⇒ _≯_ -- {x y : ℚ} → x ≤ y → x ≯ y
≤⇒≯ (*≤* p≤q) (*<* q<p) = ℤ.≤⇒≯ p≤q q<p

[mechvel]

All right. I only suggest the lemma formulations. Let the library team choose the implementation they like.
I write these rests as below, but you can rewrite them in a better way:

p*q≢0⇒p≢0 : {p q : ℚ} → p * q ≢ 0ℚ → p ≢ 0ℚ
p*q≢0⇒p≢0 {p} {q} pq≠0 p=0 =
     pq≠0
     (begin 
        p * q       ≡⟨ cong (_* q) p=0 ⟩
         0ℚ * q   ≡⟨ *-zeroˡ q ⟩
          0ℚ
     ∎)
p*q≢0⇒q≢0 : {p q : ℚ} → p * q ≢ 0ℚ → q ≢ 0ℚ
p*q≢0⇒q≢0 {p} {q} pq≠0 q=0 =
    pq≠0 
    (begin  
       p * q      ≡⟨ cong (p *_) q=0 ⟩
       p * 0ℚ   ≡⟨ *-zeroʳ p ⟩
       0ℚ
    ∎)

p*q≡0⇒p≡0∨q≡0 : {p q : ℚ} → p * q ≡ 0ℚ → p ≡ 0ℚ ⊎ q ≡ 0ℚ
p*q≡0⇒p≡0∨q≡0  {x} {y} xy=0
   with <-cmp x 0ℚ | <-cmp y 0ℚ
... |
      tri≈ _ x=0 _ | _            = inj₁ x=0
... | _            | tri≈ _ y=0 _ = inj₂ y=0
... | tri< x<0 _ _ | tri< y<0 _ _ = contradiction xy=0 (pos⇒≠0 pos-xy)
                     where
                     neg-x  = negative x<0
                     neg-y  = negative y<0
                     pos-xy = neg*neg⇒pos x {{neg-x}} y {{neg-y}}
... | tri< x<0 _ _ | tri> _ _ y>0 = contradiction xy=0 (neg⇒≠0 neg-xy)
                     where
                     neg-x  = negative x<0
                     pos-y  = positive y>0
                     neg-xy = neg*pos⇒neg x {{neg-x}} y {{pos-y}}
... | tri> _ _ x>0 | tri< y<0 _ _ = contradiction xy=0 (neg⇒≠0 neg-xy)
                     where
                     pos-x  = positive x>0
                     neg-y  = negative y<0
                     neg-xy = pos*neg⇒neg x {{pos-x}} y {{neg-y}}