\import Algebra.Domain
\import Algebra.Domain.Bezout
\import Algebra.Domain.GCD
\import Algebra.Domain.PID
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.GCD
\import Algebra.Ring
\import Algebra.Semiring
\import Arith.Int
\import Arith.Nat
\import Data.Or
\import Function.Meta
\import Logic
\import Logic.Classical
\import Logic.Meta
\import Meta
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set \hiding (#)
\import Set.Fin
\open Monoid(LDiv,Inv)

\class EuclideanSemiringData \extends CSemiring, DecSet {
  | euclideanMap : E -> Nat
  | divMod : E -> E -> \Sigma E E
  | isDivMod (x y : E) : y * (divMod x y). + (divMod x y). = x
  | isEuclideanMap (x y : E) : y /=  -> (divMod x y). /=  -> euclideanMap (divMod x y). < euclideanMap y
  | summandDiv {x y z d : E} (d/=0 : d /= ) (p : d * x + y = d * z) : LDiv d y

  \func gcd (a b : E) => gcd-fueled (suc' (euclideanMap b)) a b

  \func gcd-fueled (s : Nat) (a b : E) : E \elim s
    |  => a
    | suc s => \case decideEq b  \with {
      | yes _ => a
      | no _ => gcd-fueled s b (divMod a b).
    }

  \lemma fueled_zro (s : Nat) (a : E) : gcd-fueled s a  = a \elim s
    |  => idp
    | suc s => mcases \with {
      | yes _ => idp
      | no p => absurd (p idp)
    }

  \func reduce-fueled (s : Nat) (a b : E) : \Sigma E E \elim s
    |  => (,)
    | suc s => \case decideEq b  \with {
      | yes _ => (,)
      | no _ => \let! | (d,m) => divMod a b
                      | (a',b') => reduce-fueled s b m
                \in (a' * d + b', a')
    }

  \func reduce (a b : E) => reduce-fueled (suc' (euclideanMap b)) a b

  \lemma reduce_zro (s : Nat) (a : E) : reduce-fueled s a  = (,) \elim s
    |  => idp
    | suc s => mcases \with {
      | yes _ => idp
      | no p => absurd (p idp)
    }

  \lemma reduce*fueled-left (s : Nat) (a b : E) (b<=s : euclideanMap b < s) : (reduce-fueled s a b). * gcd-fueled s a b = a \elim s
    |  => ide-left
    | suc s => mcases \with {
      | yes _ => ide-left
      | no b/=0 => \case decideEq (divMod a b).  \with {
        | yes mod=0 => run {
          unfold_let,
          rewrite (mod=0, reduce_zro, fueled_zro, zro-right, ide-left),
          *-comm *> inv (pmap (_ +) mod=0 *> zro-right) *> isDivMod a b
        }
        | no mod/=0 => rdistr *> pmap2 (+)
            (pmap (`* _) *-comm *> *-assoc *> *-comm *> pmap (`* _) (reduce*fueled-left s b (divMod a b). (isEuclideanMap a b b/=0 mod/=0 <∘l <_suc_<= b<=s)))
            (reduce*fueled-right s b (divMod a b). (isEuclideanMap a b b/=0 mod/=0 <∘l <_suc_<= b<=s)) *> isDivMod a b
      }
    }

  \lemma reduce*fueled-right (s : Nat) (a b : E) (b<=s : euclideanMap b < s) : (reduce-fueled s a b). * gcd-fueled s a b = b \elim s
    |  => \case b<=s
    | suc s => mcases \with {
      | yes b=0 => zro_*-left *> inv b=0
      | no b/=0 => \case decideEq (divMod a b).  \with {
        | yes mod=0 => pmap2 ((reduce-fueled s b __). * gcd-fueled s b __) mod=0 mod=0 *> pmap2 (__. * __) (reduce_zro s b) (fueled_zro s b) *> ide-left
        | no mod/=0 => reduce*fueled-left s b (divMod a b). (isEuclideanMap a b b/=0 mod/=0 <∘l <_suc_<= b<=s)
      }
    }

  \lemma reduce*gcd-right (a b : E) : (reduce a b). * gcd a b = b
    => reduce*fueled-right (suc' (euclideanMap b)) a b (rewrite suc'=suc id<suc)

  \func gcd-isGCD-fueled (s : Nat) {a b g : E} (g|a : LDiv g a) (g|b : LDiv g b) : LDiv g (gcd-fueled s a b) \elim s
    |  => g|a
    | suc s => mcases \with {
      | yes _ => g|a
      | no b/=0 => gcd-isGCD-fueled s g|b (summandDiv (ldiv/=0 b/=0 g|b) (pmap (`+ _) (inv *-assoc) *> pmap (__ * _ + _) g|b.inv-right *> isDivMod a b *> inv g|a.inv-right))
    }

  \func gcd-isGCD (a b : E) : GCD a b \cowith
    | gcd => gcd a b
    | gcd|val1 => \new LDiv {
      | inv => (reduce a b).
      | inv-right => *-comm *> reduce*fueled-left (suc' (euclideanMap b)) a b (rewrite suc'=suc id<suc)
    }
    | gcd|val2 => \new LDiv {
      | inv => (reduce a b).
      | inv-right => *-comm *> reduce*gcd-right a b
    }
    | gcd-univ g g|a g|b => gcd-isGCD-fueled (suc' (euclideanMap b)) g|a g|b

  \lemma gcd_0 {x : E} : gcd x  = x
    => aux
    \where
      \lemma aux {s : Nat} {x : E} : gcd-fueled s x  = x \elim s
        |  => idp
        | suc s => mcases \with {
          | yes _ => idp
          | no n => absurd (n idp)
        }

  \func isPseudonorm {a b : E} (a/=0 : a /= ) (b|a : LDiv b a)
    => aux b a/=0 b|a id<suc
    \where
      \func aux {a : E} (b : E) (a/=0 : a /= ) (b|a : LDiv b a) {n : Nat} (p : euclideanMap a < n)
        : Or (LDiv a b) (\Sigma (b' : E) (LDiv b b') (LDiv b' b) (euclideanMap b' < euclideanMap a)) \elim n
        |  => \case p
        | suc n => \case decideEq (divMod b a).  \with {
          | yes e => inl (\new LDiv {
            | inv => (divMod b a).
            | inv-right => later (rewrite e $ inv zro-right) *> isDivMod b a
          })
          | no q => inr
            \have b|m : LDiv b (divMod b a). => summandDiv {_} {b|a.inv * (divMod b a).} (ldiv/=0 a/=0 b|a) $
                pmap (`+ _) (inv *-assoc *> later (rewrite b|a.inv-right idp)) *> isDivMod b a *> inv ide-right
            \in \case aux b q b|m (isEuclideanMap b a a/=0 q <∘l <_suc_<= p) \with {
              | inl m|b => ((divMod b a)., b|m, m|b, isEuclideanMap b a a/=0 q)
              | inr (b',b'|b,b|b',s) => (b', b'|b, b|b', s <∘ isEuclideanMap b a a/=0 q)
            }
        }

  \lemma unit-dec (a : E) (f : \Pi {b : E} -> Inv a -> b /=  -> euclideanMap a <= euclideanMap b) : Dec (Inv a)
    => \case decideEq a  \with {
         | yes a=0 => \case decideEq zro ide \with {
           | yes e => yes $ Inv.lmake  $ zro_*-left *> e
           | no q => no \lam (ai : Inv a) => q $ inv zro_*-right *> pmap (_ *) (inv a=0) *> ai.inv-left
         }
         | no a/=0 => \case decideEq (divMod  a).  \with {
           | yes q => yes $ Inv.lmake (divMod  a). $ inv zro-right *> pmap2 (+) *-comm (inv q) *> isDivMod  a
           | no q => no \lam ai => linarith (f ai q, isEuclideanMap  a a/=0 q)
         }
       }
} \where {
  \func suc' (n : Nat) : Nat
    |  => 
    | suc n => suc (suc n)

  \lemma suc'=suc (n : Nat) : suc' n = suc n
    |  => idp
    | suc n => idp
}

\open EuclideanSemiringData

\class EuclideanRingData \extends EuclideanSemiringData, CRing {
  | summandDiv {x} {y} {z} {d} _ p => \new LDiv {
    | inv => z - x
    | inv-right => ldistr *> +-comm *> pmap (+ _) (inv p) *> simplify
  }

  \func bezout-fueled (s : Nat) (a b : E) : \Sigma E E \elim s
    |  => (,)
    | suc s => \case decideEq b  \with {
      | yes _ => (,)
      | no _ => \let! | (d,m) => divMod a b
                      | (u,v) => bezout-fueled s b m
                \in (v, u - d * v)
    }

  \func bezout (a b : E) => bezout-fueled (suc' (euclideanMap b)) a b

  \lemma bezoutIdentity-fueled (s : Nat) (a b : E) : (bezout-fueled s a b). * a + (bezout-fueled s a b). * b = gcd-fueled s a b \elim s
    |  => simplify
    | suc s => mcases \with {
      | yes _ => simplify
      | no _ => pmap (_ * __ + _) (inv (isDivMod a b)) *> equation *> bezoutIdentity-fueled s b (divMod a b).
    }

  \lemma bezoutIdentity (a b : E) : (bezout a b). * a + (bezout a b). * b = gcd a b
    => bezoutIdentity-fueled (suc' (euclideanMap b)) a b
}

\class EuclideanDomain \extends PID
  | isEuclidean : TruncP (EuclideanRingData { | CRing => \this | decideEq => decideEq })
  | isBezout a b => TruncP.map isEuclidean \lam (d : EuclideanRingData { | CRing => \this }) =>
      ((d.bezout a b)., (d.bezout a b).,
       rewrite d.bezoutIdentity (GCD.gcd|val1 {d.gcd-isGCD a b}),
       rewrite d.bezoutIdentity (GCD.gcd|val2 {d.gcd-isGCD a b}))
  | divChain a c => \case isEuclidean \with {
    | inP d => cases (a  arg addPath) \with {
      | in~ a0, ap =>
        \let n => suc (euclideanMap {d} a0.)
        \in \case Choice.liftSurj {FinFin (suc n)} Quotient.in-surj (\lam j => a j) \with {
          | inP (b,bp) => TruncP.map (aux {d} n (\lam i => ((b i)., AddGroup.With#.apartNonZero (b i).))
              (\lam i => TruncP.map (c i) \lam ci => nonZero_ldiv {_} {b (suc i)} {b i} $ div-from~ {nonZeroMonoid} $ rewrite (bp (suc i), bp i) ci) a0.
              (nonZero_ldiv {_} {b } {a0} $ div-from~ {nonZeroMonoid} $ rewrite (bp , ap) LDiv.id-div)
              (nonZero_ldiv {_} {a0} {b } $ div-from~ {nonZeroMonoid} $ rewrite (bp , ap) LDiv.id-div)
              id<suc) \lam s => (s., rewriteI (bp s., bp (suc s.)) $ div-to~ {nonZeroMonoid} $ ldiv_nonZero s.)
        }
    }
  }
  \where {
    \open DivQuotient

    \lemma aux {R : EuclideanRingData} (n : Nat) (a : Fin (suc n) -> \Sigma (x : R) (x /= )) (c : \Pi (i : Fin n) -> TruncP (LDiv (a (suc i)). (a i).)) (b : R) (a0|b : LDiv (a ). b) (b|a0 : LDiv b (a ).) (p : euclideanMap b < n) : ∃ (i : Fin n) (LDiv (a i). (a (suc i)).) \elim n
      |  => \case p
      | suc n => \case c  \with {
        | inP c0 => \case isPseudonorm {_} {b} {(a ).} (ldiv/=0 (a ). b|a0) (LDiv.trans c0 a0|b) \with {
          | inl b|a1 => inP (, LDiv.trans a0|b b|a1)
          | inr (a1',a1|a1',a1'|a1,a1'<b) => TruncP.map (aux n (\lam i => a (suc i)) (\lam i => c (suc i)) a1' a1|a1' a1'|a1 (a1'<b <∘l <_suc_<= p)) \lam s => (suc s., s.)
        }
      }
  }

\instance NatEuclidean : EuclideanSemiringData
  | CSemiring => NatSemiring
  | euclideanMap n => n
  | divMod => divMod
  | isDivMod => divModProp
  | isEuclideanMap n m m/=0 _ => \case \elim m, m/=0 \with {
    | , c => absurd (c idp)
    | suc m, _ => fin_< (n mod suc m)
  }
  | decideEq => NatSemiring.decideEq
  | summandDiv {x y z d : Nat} (d/=0 : d /= ) (dx+y=dz : d * x + y = d * z) : Monoid.LDiv d y \elim d {
    |  => absurd (d/=0 idp)
    | suc _ \as d => \new Monoid.LDiv {
      | inv => div y d
      | inv-right => pmap (d * y div d +) (mod-unique {d} {z} {} {x + y div d} {y mod d} NatSemiring.zero<suc (fin_< (y mod d)) (inv (pmap (`+ _) ldistr *> +-assoc *> pmap (_ +) (divModProp y d) *> dx+y=dz))) *> divModProp y d
    }
  }
  \where {
    \open Nat

    \lemma gcd0_ {x : Nat} : NatEuclidean.gcd  x = x \elim x
      |  => idp
      | suc x => idp
  }

\instance IntEuclidean : EuclideanRingData
  | CRing => IntRing
  | decideEq => IntRing.decideEq
  | euclideanMap => iabs
  | divMod x y =>
    \let! (d,m) => Nat.divMod (iabs x) (iabs y)
    \in (pos d * signum y * signum x, pos m * signum x)
  | isDivMod (x y : Int) : y * (pos (iabs x Nat.div iabs y) * signum y * signum x) + pos (iabs x Nat.mod iabs y) * signum x = x \with {
    | pos , y => simplify
    | pos (suc n), pos  => idp
    | neg (suc n), pos  => idp
    | pos (suc _ \as n), pos (suc _ \as m) => pmap pos (Nat.divModProp n m)
    | pos (suc _ \as n), neg (suc _ \as m) => pmap (_ * __ + _) ide-right *> pmap pos (Nat.divModProp n m)
    | neg (suc _ \as n), pos (suc _ \as m) => pmap neg (Nat.divModProp n m)
    | neg (suc _ \as n), neg (suc _ \as m) => pmap (_ * __ + _) (Ring.negative_*-left {_} {pos (n Nat.div m)}) *> pmap neg (Nat.divModProp n m)
  }
  | isEuclideanMap x y y/=0 r/=0 =>
    \have |y|/=0 : iabs y /=  => \case \elim y, y/=0 \with {
      | , c => \lam _ => c idp
      | pos (suc _), c => \lam y=0 => c (pmap pos y=0)
      | neg (suc _), c => \lam y=0 => c (pmap neg y=0)
    }
    \in \case decideEq (signum x)  \with {
      | yes x=0 => rewrite x=0 (nonZero>0 |y|/=0)
      | no x/=0 =>
        \have t : iabs (pos (iabs x Nat.mod iabs y) * signum x) = iabs x Nat.mod iabs y => iabs_* *> pmap (_ *) (iabs.signum_/=0 (x/=0 $ pmap signum __))
        \in transport (`< iabs y) (inv t) $ isEuclideanMap (iabs x) (iabs y) |y|/=0 \lam e => r/=0 $ pmap (pos __ * _) e *> zro_*-left
    }
  \where {
    \func modToNat (m : Int) (p : \Sigma Int Int) : \Sigma Int Nat \elim p
      | (q, pos n) => (q, n)
      | (q, neg (suc n)) => (q - signum m, iabs (iabs m Nat.- suc n))

    \func natDivMod (x y : Int) : \Sigma Int Nat
      => modToNat y (IntEuclidean.divMod x y)

    \func \infixl  div (x y : Int) : Int
      => (natDivMod x y).

    \func \infixl  mod (x y : Int) : Nat
      => (natDivMod x y).

    \lemma intMod<right (x : Int) (n : Nat) : iabs (IntEuclidean.divMod x (suc n)). < suc n
      => \case decideEq (IntEuclidean.divMod x (suc n)).  \with {
        | yes e => rewrite e NatSemiring.zero<suc
        | no e => IntEuclidean.isEuclideanMap x (suc n) (\case __) e
      }

    \lemma natMod<right (x : Int) (n : Nat) : x mod suc n < suc n
      => \let (q,r) => IntEuclidean.divMod x (suc n)
         \in \case r \as r, idp : r = (IntEuclidean.divMod x (suc n)). \return (modToNat (suc n) (q,r)). < suc n \with {
               | pos m, p => transportInv (`< suc n) (pmap iabs p) (intMod<right x n)
               | neg (suc m), p => pos<=pos.conv (transportInv (`<= pos n) (pos_iabs (<=-less (transportInv (`< suc n) (pmap iabs p) (intMod<right x n)))) (IntRing.<=_+ {pos n} {n} {neg m} {} <=-refl (signum.signum_neg/=1 __))) <∘r id<suc
             }

    \lemma divModProp (x y : Int) (y/=0 : y /= ) : y * x div y + x mod y = x
      => \let (q,r) => IntEuclidean.divMod x y
         \in \case r \as r, idp : r = (IntEuclidean.divMod x y). \return y * (modToNat y (q,r)). + (modToNat y (q,r)). = x \with {
               | pos n, p => pmap (y * q + __) p *> IntEuclidean.isDivMod x y
               | neg (suc n), p =>
                 \have t : iabs (pos (iabs x Nat.mod iabs y) * signum x) = iabs x Nat.mod iabs y =>
                     \case decideEq x  \with {
                       | yes x=0 => rewrite x=0 idp
                       | no x/=0 => iabs_* *> pmap (_ *) (iabs.signum_/=0 x/=0)
                     }
                 \in pmap (_ +) (pos_iabs $ transportInv (`<= iabs y) (pmap iabs p) $ transportInv (`<= iabs y) t $ <=-less $ mod<right \lam |y|=0 => y/=0 $ iabs.equals0 |y|=0) *>
                     pmap (`+ _) Ring.ldistr_- *>
                     pmap ((_ + negative __) + _) (inv iabs.signum_*) *>
                     +-assoc *>
                     pmap (_ +) (inv (+-assoc {_} {_} {pos (iabs y)} {neg (suc n)}) *> pmap (`+ _) (IntRing.negative-right {iabs y})) *>
                     pmap (_ +) p *>
                     IntEuclidean.isDivMod x y
             }

    \lemma natDivModProp (x : Int) (n : Nat) : pos (suc n) * x div suc n + x mod suc n = x
      => divModProp x (suc n) (\case __)

    \lemma mod-unique {q q' : Int} {n r r' : Nat} (r<n : r < n) (r'<n : r' < n) (p : pos n * q + r = pos n * q' + r') : r = r' \elim q, q'
      | pos q, pos q' => Arith.Nat.mod-unique r<n r'<n (pmap iabs p)
      | pos q, neg q' => Arith.Nat.mod-unique {n} {q' + q} {r} {} r<n r'<n (pmap iabs (pmap (`+ pos r) (IntRing.ldistr {n} {q'} {q}) *> aux (pos (n * q)) r (pos (n * q')) r' p))
      | neg q, pos q' => inv (Arith.Nat.mod-unique {n} {q + q'} {r'} {} r'<n r<n (pmap iabs (pmap (`+ pos r') (IntRing.ldistr {n} {q} {q'}) *> aux (pos (n * q')) r' (pos (n * q)) r (inv p))))
      | neg q, neg q' => inv (Arith.Nat.mod-unique r'<n r<n (pmap iabs (aux  r' (n * q) (n * q' + r) (inv (aux (neg (n * q)) r (n * q') r' p) *> IntRing.+-assoc {neg (n * q)} {n * q'} {r}) )))
      \where
        \lemma aux (x y x' y' : Int) (p : x + y = negative x' + y') : (x' + x) + y = y'
          => +-assoc *> pmap (x' +) p *> simplify

    \lemma natMod=mod' (x n : Nat) : (IntEuclidean.divMod x n). = x Nat.mod n \elim x
      |  => idp
      | suc x => idp

    \lemma natMod=mod (x n : Nat) : x mod n = x Nat.mod n \elim x
      |  => idp
      | suc x => idp
  }

\instance IntDomain : EuclideanDomain
  | CRing => IntRing
  | zro#ide => \case __
  | #0-* {x y : Int} (x/=0 : x /= ) (y/=0 : y /= ) : x * y /=  \elim x, y {
    | pos , _ => \lam _ => x/=0 idp
    | pos _, pos  => \lam _ => y/=0 idp
    | neg _, pos  => \lam _ => y/=0 idp
    | pos (suc n), pos (suc m) => \case __
    | pos (suc n), neg (suc m) => \case __
    | neg (suc n), pos (suc m) => \case __
    | neg (suc n), neg (suc m) => \case __
  }
  | decideEq => IntRing.decideEq
  | isEuclidean => inP IntEuclidean

\lemma ldiv_nat_int (d : LDiv {NatSemiring}) : LDiv (pos d.val) (pos d.elem) (pos d.inv) \cowith
  | inv-right => pmap pos d.inv-right

\lemma ldiv_int_nat (d : LDiv {IntRing}) : LDiv (iabs d.val) (iabs d.elem) (iabs d.inv) \cowith
  | inv-right => inv iabs_* *> pmap iabs d.inv-right

\lemma inv_nat_int (d : Inv {NatSemiring}) : Inv (pos d.val) (pos d.inv) \cowith
  | inv-left => pmap pos d.inv-left
  | inv-right => pmap pos d.inv-right

\lemma inv_int_nat (d : Inv {IntRing}) : Inv (iabs d.val) (iabs d.inv) \cowith
  | inv-left => inv iabs_* *> pmap iabs d.inv-left
  | inv-right => inv iabs_* *> pmap iabs d.inv-right

\lemma inv_abs {x : Int} (d : Inv (iabs x)) : Inv x
  => Inv.lmake (pos d.inv * signum x) (*-assoc *> pmap (_ *) (*-comm *> inv iabs.signum_*) *> pmap pos d.inv-left)

\func gcd_nat_int (g : GCD {NatSemiring}) : GCD (pos g.val1) (pos g.val2) (pos g.gcd) \cowith
  | gcd|val1 => ldiv_nat_int g.gcd|val1
  | gcd|val2 => ldiv_nat_int g.gcd|val2
  | gcd-univ g' g'|a g'|b =>
    \have abs_g'|g : LDiv (iabs g') g.gcd => g.gcd-univ (iabs g') (ldiv_int_nat g'|a) (ldiv_int_nat g'|b)
    \in \new LDiv {
      | inv => signum g' * abs_g'|g.inv
      | inv-right => inv *-assoc *> pmap (`* _) (inv iabs.signum_*) *> pmap pos abs_g'|g.inv-right
    }

\func gcd_int_nat (g : GCD {IntRing}) : GCD (iabs g.val1) (iabs g.val2) (iabs g.gcd) \cowith
  | gcd|val1 => ldiv_int_nat g.gcd|val1
  | gcd|val2 => ldiv_int_nat g.gcd|val2
  | gcd-univ g' (g'|a : LDiv) (g'|b : LDiv) =>
    \have pos_g'|g : LDiv (pos g') g.gcd => g.gcd-univ (pos g')
        (\new LDiv {
          | inv => pos g'|a.inv * signum g.val1
          | inv-right => inv *-assoc *> pmap (pos __ * _) g'|a.inv-right *> iabs.*_signum
        })
        (\new LDiv {
          | inv => pos g'|b.inv * signum g.val2
          | inv-right => inv *-assoc *> pmap (pos __ * _) g'|b.inv-right *> iabs.*_signum
        })
    \in \new LDiv {
      | inv => iabs pos_g'|g.inv
      | inv-right => inv iabs_* *> pmap iabs pos_g'|g.inv-right
    }

\lemma nat_gcd-isUnique {n m : Nat} (g g' : GCD n m) : g.gcd = g'.gcd
  => natAssociates-areEqual (g'.gcd-univ g.gcd g.gcd|val1 g.gcd|val2) (g.gcd-univ g'.gcd g'.gcd|val1 g'.gcd|val2)

\lemma int_gcd-isUnique {x y : Int} (g g' : GCD x y) : iabs g.gcd = iabs g'.gcd
  => nat_gcd-isUnique (gcd_int_nat g) (gcd_int_nat g')

\lemma int_gcd_pos {n m : Nat} : gcd (pos n) (pos m) = pos (gcd n m)
  => aux (suc' m) *> pmap pos (int_gcd-isUnique (gcd-isGCD (pos n) (pos m)) (gcd_nat_int (gcd-isGCD n m)))
  \where {
    \lemma aux (s : Nat) {n m : Nat} : gcd-fueled s (pos n) (pos m) = iabs (gcd-fueled s (pos n) (pos m)) \elim s
      |  => idp
      | suc s => mcases \with {
        | yes _ => idp
        | no _ => rewrite IntEuclidean.natMod=mod' (aux s)
      }
  }

\lemma nat_gcd_sum (a b d : Nat) : gcd (a + b * d) b = gcd a b
  => \let a' => a + b * d
     \in equation                     #'
         gcd a' b                     #' {nat_gcd-isUnique (gcd-isGCD a' b) (gcd_int_nat (gcd-isGCD (pos a') (pos b)))}
         iabs (gcd (pos a') (pos b))  #' {int_gcd-isUnique (gcd-isGCD (pos a') (pos b)) (GCDDomain.gcd_sum (pos d) (gcd-isGCD (pos a) (pos b)))}
         iabs (gcd (pos a) (pos b))   #' {inv (nat_gcd-isUnique (gcd-isGCD a b) (gcd_int_nat (gcd-isGCD (pos a) (pos b))))}
         gcd a b

\func nat_gcd_*_div {a b c : Nat} (a|bc : LDiv a (b * c)) (a_b : gcd a b = ) : LDiv a c
  => ldiv_int_nat $ Domain.Dec.LDiv_TruncP $ GCDMonoid.coprime_*_div {IntDomain} {pos a} {pos b} {pos c} (ldiv_nat_int a|bc) $ IsCoprime.<=gcd $ gcd_nat_int $ transport (GCD a b __) a_b (gcd-isGCD a b)

\lemma nat_gcd-comm {a b : Nat} : gcd a b = gcd b a
  => nat_gcd-isUnique (gcd-isGCD a b) (GCD.swap {gcd-isGCD b a})