coprime-lemma

coprime

module kyoin-test where

open import Data.Bool.Properties
open import Data.Nat
open import Data.Nat.Properties.Simple
open import Data.Nat.Coprimality as Coprime
open import Data.Nat.Divisibility
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Nullary.Sum
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum
open import Data.Empty
open import Function using (_∘_; _$_)

a+b≡c⇒b+a≡c : ∀ a b c → a + b ≡ c → b + a ≡ c
a+b≡c⇒b+a≡c a b c prf rewrite +-comm a b = prf

a*b≡c⇒b*a≡c : ∀ a b c → a * b ≡ c → b * a ≡ c
a*b≡c⇒b*a≡c a b c prf rewrite *-comm a b = prf

comm-∣+ : ∀ i a b → i ∣ a + b → i ∣ b + a
comm-∣+ i a b (divides q a+b≡q*i) = divides q (a+b≡c⇒b+a≡c a b (q * i) a+b≡q*i)

comm-∣* : ∀ i a b → i ∣ a * b → i ∣ b * a
comm-∣* i a b (divides q a*b≡q*i) = divides q (a*b≡c⇒b*a≡c a b (q * i) a*b≡q*i)

i∣a+b∧i∣a*b⇒i∣a⊎i∣b : ∀ i a b → Coprime a b → i ∣ a + b × i ∣ a * b → i ∣ a ⊎ i ∣ b
i∣a+b∧i∣a*b⇒i∣a⊎i∣b i a b c (i∣a+b , i∣a*b) with i ∣? a ⊎-dec i ∣? b
i∣a+b∧i∣a*b⇒i∣a⊎i∣b i a b c (i∣a+b , i∣a*b) | yes i∣a⊎i∣b = i∣a⊎i∣b
i∣a+b∧i∣a*b⇒i∣a⊎i∣b i a b c (i∣a+b , i∣a*b) | no ¬i∣a⊎i∣b = {!!}

lemma : ∀ a b → Coprime a b → Coprime (a + b) (a * b)
lemma a b c {i} (i∣a+b , i∣a*b)
  = c (i∣a+b∧i∣a*b→i∣a i a b c (i∣a+b , i∣a*b) , i∣a+b∧i∣a*b→i∣b i a b c (i∣a+b , i∣a*b))
  where
    i∣a+b∧i∣a*b→i∣a : ∀ i a b → Coprime a b → (i ∣ a + b) × (i ∣ a * b) → i ∣ a
    i∣a+b∧i∣a*b→i∣a i a b c (i∣a+b , i∣a*b) with i∣a+b∧i∣a*b⇒i∣a⊎i∣b i a b c (i∣a+b , i∣a*b)
    ... | inj₁ i∣a = i∣a
    ... | inj₂ i∣b = ∣-∸ (comm-∣+ i a b i∣a+b) i∣b

    i∣a+b∧i∣a*b→i∣b : ∀ i a b → Coprime a b → (i ∣ a + b) × (i ∣ a * b) → i ∣ b
    i∣a+b∧i∣a*b→i∣b i a b c (i∣a+b , i∣a*b)
      = i∣a+b∧i∣a*b→i∣a i b a (Coprime.sym c) ((comm-∣+ i a b i∣a+b) , comm-∣* i a b i∣a*b)