Hoping to prove some things about modular congruences

Mod.idr

%default total

{-
A few notes:
* I think maybe this should be called a Quotient Type
* There's a few fns where I'd ike to pattern match on n=(m ** prf) but instead am using fst and snd
-}

data Mod : (m ** Not (m = Z)) -> Type where
  MkMod : (n : Nat) -> Mod m

simplify : Mod n -> Mod n
simplify (MkMod k) = MkMod (modNatNZ k (fst n) (snd n))

difference : Nat -> Nat -> Nat
difference Z Z = 0
difference Z j = j
difference k Z = k
difference (S k) (S j) = difference k j

implementation Eq (Mod n) where
  (==) (MkMod k) (MkMod j) = modNatNZ (difference k j) (fst n) (snd n) == Z

(+) : Mod m -> Mod m -> Mod m
(+) (MkMod x) (MkMod y) = MkMod (x+y)

modRefl : (x : Mod m) -> x = x
modRefl x = Refl

modSym : (x : Mod m) -> (y : Mod m) -> x = y -> y = x
modSym x x Refl = Refl

modTrans : (x : Mod m) -> (y : Mod m) -> (z : Mod m) -> x = y -> y = z -> x = z
modTrans x x x Refl Refl = Refl

modInjective : (x : Nat) -> (y : Nat)  -> x = y -> (MkMod x) = (MkMod y)
modInjective x x Refl = Refl

modPlusCommutes : (x' : Mod m) -> (y' : Mod m) -> x'+y' = y'+x'
modPlusCommutes (MkMod j) (MkMod k) = modInjective _ _ (plusCommutative _ _)

modTranslate : (a : Mod m) -> (b : Mod m) -> (k : Mod m) -> a = b -> (a+k) = (b+k)
modTranslate a a k Refl = Refl

modPlusZeroRightNeutral : (a : Mod m) -> a + (MkMod 0) = a
modPlusZeroRightNeutral (MkMod n) = modInjective _ _ (plusZeroRightNeutral _)

modPlusZeroLeftNeutral : (a : Mod m) -> (MkMod 0) + a = a
modPlusZeroLeftNeutral a = rewrite modPlusCommutes (MkMod 0) a in
                                   modPlusZeroRightNeutral a

(*) : Mod m -> Mod m -> Mod m
(*) (MkMod x) (MkMod y) = MkMod (x*y)

{--
implementation Ord (Mod m) where
  compare j k = case (simplify j, simplify k) of
                     (MkMod j', MkMod k') => compare j' k'

-- I really don't like these nested case statements
(-) : Mod m -> Mod m -> Mod m
(-) x y = case (simplify x, simplify y) of
                 (MkMod a', MkMod b') => (case m of
                                               (n ** pf) => (case a' < b' of
                                                                  False => MkMod (minus a' b')
                                                                  True => MkMod (a' + (minus n b'))))
--}

For example, 7+11 (mod 13) is encoded as:
(MkMod {m=(13 ** SIsNotZ)} 7) + (MkMod 11)