{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Data.Nat.DivMod where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Nat
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.Fin.Properties
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Nat.DivMod.Core
import qualified MAlonzo.Code.Data.Nat.Divisibility.Core
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Induction.WellFounded
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Core
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Syntax
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Data.Nat.DivMod.m≡m%n+[m/n]*n
d_m'8801'm'37'n'43''91'm'47'n'93''42'n_20 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'8801'm'37'n'43''91'm'47'n'93''42'n_20 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_m'8801'm'37'n'43''91'm'47'n'93''42'n_20 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m%n≡m∸m/n*n
d_m'37'n'8801'm'8760'm'47'n'42'n_32 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'37'n'8801'm'8760'm'47'n'42'n_32 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_m'37'n'8801'm'8760'm'47'n'42'n_32 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod._.m/n*n
d_m'47'n'42'n_42 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_m'47'n'42'n_42 :: Integer -> Integer -> T_NonZero_112 -> Integer
d_m'47'n'42'n_42 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du_m'47'n'42'n_42 Integer
v0 Integer
v1
du_m'47'n'42'n_42 :: Integer -> Integer -> Integer
du_m'47'n'42'n_42 :: Integer -> Integer -> Integer
du_m'47'n'42'n_42 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
      Integer -> Integer -> Integer
mulInt
      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
      (Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Nat.DivMod.%-congˡ
d_'37''45'cong'737'_48 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'37''45'cong'737'_48 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
d_'37''45'cong'737'_48 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.%-congʳ
d_'37''45'cong'691'_54 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'37''45'cong'691'_54 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
d_'37''45'cong'691'_54 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.n%1≡0
d_n'37'1'8801'0_58 ::
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_n'37'1'8801'0_58 :: Integer -> T__'8801'__12
d_n'37'1'8801'0_58 = Integer -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.n%n≡0
d_n'37'n'8801'0_64 ::
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_n'37'n'8801'0_64 :: Integer -> T_NonZero_112 -> T__'8801'__12
d_n'37'n'8801'0_64 = Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m%n%n≡m%n
d_m'37'n'37'n'8801'm'37'n_74 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'37'n'37'n'8801'm'37'n_74 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_m'37'n'37'n'8801'm'37'n_74 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.[m+n]%n≡m%n
d_'91'm'43'n'93''37'n'8801'm'37'n_86 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'91'm'43'n'93''37'n'8801'm'37'n_86 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_'91'm'43'n'93''37'n'8801'm'37'n_86 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.[m+kn]%n≡m%n
d_'91'm'43'kn'93''37'n'8801'm'37'n_100 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'91'm'43'kn'93''37'n'8801'm'37'n_100 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_'91'm'43'kn'93''37'n'8801'm'37'n_100 = Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m≤n⇒[n∸m]%m≡n%m
d_m'8804'n'8658''91'n'8760'm'93''37'm'8801'n'37'm_118 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'8804'n'8658''91'n'8760'm'93''37'm'8801'n'37'm_118 :: Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
d_m'8804'n'8658''91'n'8760'm'93''37'm'8801'n'37'm_118 = Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m*n≤o⇒[o∸m*n]%n≡o%n
d_m'42'n'8804'o'8658''91'o'8760'm'42'n'93''37'n'8801'o'37'n_136 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'42'n'8804'o'8658''91'o'8760'm'42'n'93''37'n'8801'o'37'n_136 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8801'__12
d_m'42'n'8804'o'8658''91'o'8760'm'42'n'93''37'n'8801'o'37'n_136
  = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m*n%n≡0
d_m'42'n'37'n'8801'0_154 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'42'n'37'n'8801'0_154 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_m'42'n'37'n'8801'0_154 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m%n<n
d_m'37'n'60'n_166 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'37'n'60'n_166 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22
d_m'37'n'60'n_166 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> T__'8804'__22
du_m'37'n'60'n_166 Integer
v0 Integer
v1
du_m'37'n'60'n_166 ::
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'37'n'60'n_166 :: Integer -> Integer -> T__'8804'__22
du_m'37'n'60'n_166 Integer
v0 Integer
v1
  = let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
    Any -> T__'8804'__22
forall a b. a -> b
coe
      ((T__'8804'__22 -> T__'8804'__22) -> T__'8804'__22 -> Any
forall a b. a -> b
coe
         T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Base.C_s'8804's_34
         (Integer -> Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.DivMod.Core.d_a'91'mod'8341''93'n'60'n_70
            (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v2)))
-- Data.Nat.DivMod.m%n≤n
d_m'37'n'8804'n_178 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'37'n'8804'n_178 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22
d_m'37'n'8804'n_178 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> T__'8804'__22
du_m'37'n'8804'n_178 Integer
v0 Integer
v1
du_m'37'n'8804'n_178 ::
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'37'n'8804'n_178 :: Integer -> Integer -> T__'8804'__22
du_m'37'n'8804'n_178 Integer
v0 Integer
v1
  = (T__'8804'__22 -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
      T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854
      ((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T__'8804'__22
du_m'37'n'60'n_166 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
-- Data.Nat.DivMod.m%n≤m
d_m'37'n'8804'm_190 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'37'n'8804'm_190 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22
d_m'37'n'8804'm_190 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> T__'8804'__22
du_m'37'n'8804'm_190 Integer
v0 Integer
v1
du_m'37'n'8804'm_190 ::
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'37'n'8804'm_190 :: Integer -> Integer -> T__'8804'__22
du_m'37'n'8804'm_190 Integer
v0 Integer
v1
  = let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
    Any -> T__'8804'__22
forall a b. a -> b
coe
      ((Integer -> Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
         Integer -> Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.DivMod.Core.d_a'91'mod'8341''93'n'8804'a_96
         (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
-- Data.Nat.DivMod.m≤n⇒m%n≡m
d_m'8804'n'8658'm'37'n'8801'm_196 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'8804'n'8658'm'37'n'8801'm_196 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12
d_m'8804'n'8658'm'37'n'8801'm_196 = Integer -> Integer -> T__'8804'__22 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m<n⇒m%n≡m
d_m'60'n'8658'm'37'n'8801'm_210 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'60'n'8658'm'37'n'8801'm_210 :: Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
d_m'60'n'8658'm'37'n'8801'm_210 = Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.%-pred-≡0
d_'37''45'pred'45''8801'0_220 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'37''45'pred'45''8801'0_220 :: Integer
-> Integer -> T_NonZero_112 -> T__'8801'__12 -> T__'8801'__12
d_'37''45'pred'45''8801'0_220 = Integer
-> Integer -> T_NonZero_112 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m<[1+n%d]⇒m≤[n%d]
d_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_236 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_236 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
d_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_236 ~Integer
v0 Integer
v1 Integer
v2
                                                          ~T_NonZero_112
v3
  = Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_236 Integer
v1 Integer
v2
du_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_236 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_236 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_236 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> (Any -> Any) -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe (\ Any
v2 -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe
             ((Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.DivMod.Core.du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216
                (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
-- Data.Nat.DivMod.[1+m%d]≤1+n⇒[m%d]≤n
d_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_252 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_252 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
d_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_252 Integer
v0
                                                                 ~Integer
v1 Integer
v2 ~T_NonZero_112
v3 ~T__'8804'__22
v4
  = Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_252
      Integer
v0 Integer
v2
du_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_252 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_252 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_252 Integer
v0
                                                                  Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> (Any -> Any) -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe (\ Any
v2 -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe
             ((Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.DivMod.Core.du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260
                (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
-- Data.Nat.DivMod.%-distribˡ-+
d_'37''45'distrib'737''45''43'_270 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'37''45'distrib'737''45''43'_270 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_'37''45'distrib'737''45''43'_270 = Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.%-distribˡ-*
d_'37''45'distrib'737''45''42'_300 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'37''45'distrib'737''45''42'_300 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_'37''45'distrib'737''45''42'_300 = Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod._.m′
d_m'8242'_312 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_m'8242'_312 :: Integer
-> Integer -> Integer -> T_NonZero_112 -> T_NonZero_112 -> Integer
d_m'8242'_312 Integer
v0 ~Integer
v1 Integer
v2 ~T_NonZero_112
v3 = Integer -> Integer -> T_NonZero_112 -> Integer
du_m'8242'_312 Integer
v0 Integer
v2
du_m'8242'_312 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
du_m'8242'_312 :: Integer -> Integer -> T_NonZero_112 -> Integer
du_m'8242'_312 Integer
v0 Integer
v1 T_NonZero_112
v2
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Nat.DivMod._.n′
d_n'8242'_314 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_n'8242'_314 :: Integer
-> Integer -> Integer -> T_NonZero_112 -> T_NonZero_112 -> Integer
d_n'8242'_314 ~Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 = Integer -> Integer -> T_NonZero_112 -> Integer
du_n'8242'_314 Integer
v1 Integer
v2
du_n'8242'_314 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
du_n'8242'_314 :: Integer -> Integer -> T_NonZero_112 -> Integer
du_n'8242'_314 Integer
v0 Integer
v1 T_NonZero_112
v2
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Nat.DivMod._.k
d_k_316 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_k_316 :: Integer
-> Integer -> Integer -> T_NonZero_112 -> T_NonZero_112 -> Integer
d_k_316 Integer
v0 ~Integer
v1 Integer
v2 ~T_NonZero_112
v3 = Integer -> Integer -> T_NonZero_112 -> Integer
du_k_316 Integer
v0 Integer
v2
du_k_316 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
du_k_316 :: Integer -> Integer -> T_NonZero_112 -> Integer
du_k_316 Integer
v0 Integer
v1 T_NonZero_112
v2
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Nat.DivMod._.j
d_j_318 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_j_318 :: Integer
-> Integer -> Integer -> T_NonZero_112 -> T_NonZero_112 -> Integer
d_j_318 ~Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 = Integer -> Integer -> T_NonZero_112 -> Integer
du_j_318 Integer
v1 Integer
v2
du_j_318 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
du_j_318 :: Integer -> Integer -> T_NonZero_112 -> Integer
du_j_318 Integer
v0 Integer
v1 T_NonZero_112
v2
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Nat.DivMod._.lemma
d_lemma_320 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemma_320 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_lemma_320 = Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.%-remove-+ˡ
d_'37''45'remove'45''43''737'_340 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'37''45'remove'45''43''737'_340 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
d_'37''45'remove'45''43''737'_340 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.%-remove-+ʳ
d_'37''45'remove'45''43''691'_360 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'37''45'remove'45''43''691'_360 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
d_'37''45'remove'45''43''691'_360 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod./-congˡ
d_'47''45'cong'737'_372 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'47''45'cong'737'_372 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
d_'47''45'cong'737'_372 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod./-congʳ
d_'47''45'cong'691'_378 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'47''45'cong'691'_378 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
d_'47''45'cong'691'_378 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.0/n≡0
d_0'47'n'8801'0_384 ::
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_0'47'n'8801'0_384 :: Integer -> T_NonZero_112 -> T__'8801'__12
d_0'47'n'8801'0_384 = Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.n/1≡n
d_n'47'1'8801'n_388 ::
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_n'47'1'8801'n_388 :: Integer -> T__'8801'__12
d_n'47'1'8801'n_388 = Integer -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.n/n≡1
d_n'47'n'8801'1_396 ::
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_n'47'n'8801'1_396 :: Integer -> T_NonZero_112 -> T__'8801'__12
d_n'47'n'8801'1_396 = Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m*n/n≡m
d_m'42'n'47'n'8801'm_406 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'42'n'47'n'8801'm_406 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_m'42'n'47'n'8801'm_406 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m/n*n≡m
d_m'47'n'42'n'8801'm_418 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'47'n'42'n'8801'm_418 :: Integer
-> Integer -> T_NonZero_112 -> T__'8739'__20 -> T__'8801'__12
d_m'47'n'42'n'8801'm_418 = Integer
-> Integer -> T_NonZero_112 -> T__'8739'__20 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m*[n/m]≡n
d_m'42''91'n'47'm'93''8801'n_428 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'42''91'n'47'm'93''8801'n_428 :: Integer
-> Integer -> T_NonZero_112 -> T__'8739'__20 -> T__'8801'__12
d_m'42''91'n'47'm'93''8801'n_428 = Integer
-> Integer -> T_NonZero_112 -> T__'8739'__20 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m/n*n≤m
d_m'47'n'42'n'8804'm_440 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'47'n'42'n'8804'm_440 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22
d_m'47'n'42'n'8804'm_440 Integer
v0 Integer
v1 ~T_NonZero_112
v2
  = Integer -> Integer -> T__'8804'__22
du_m'47'n'42'n'8804'm_440 Integer
v0 Integer
v1
du_m'47'n'42'n'8804'm_440 ::
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'47'n'42'n'8804'm_440 :: Integer -> Integer -> T__'8804'__22
du_m'47'n'42'n'8804'm_440 Integer
v0 Integer
v1
  = ((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> T__'8804'__22
forall a b. a -> b
coe
      (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> T__IsRelatedTo__78
 -> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
         (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
         (\ Any
v2 Any
v3 Any
v4 ->
            (T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854 Any
v4))
      (Integer -> Integer -> Integer
mulInt
         ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
         (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
      Integer
v0
      (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
         ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> Any -> (Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
            T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
            (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
            (\ Any
v2 Any
v3 Any
v4 Any
v5 Any
v6 ->
               (T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
                 T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986 Any
v5
                 Any
v6))
         (Integer -> Integer -> Integer
mulInt
            ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
            (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
         (Integer -> Integer -> Integer
addInt
            ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
            ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
               Integer -> Integer -> Integer
mulInt
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
               (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
         Integer
v0
         (((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
            (Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
            (\ Any
v2 Any
v3 Any
v4 Any
v5 Any
v6 -> Any
v6)
            (Integer -> Integer -> Integer
addInt
               ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
               ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
                  Integer -> Integer -> Integer
mulInt
                  ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                  (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
            (Integer -> Integer -> Integer
addInt
               ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
               ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
                  Integer -> Integer -> Integer
mulInt
                  ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                  (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
            Integer
v0
            (((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
               (Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
               (\ Any
v2 Any
v3 Any
v4 Any
v5 Any
v6 -> Any
v6)
               (Integer -> Integer -> Integer
addInt
                  ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                  ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
                     Integer -> Integer -> Integer
mulInt
                     ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                     (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
               Integer
v0 Integer
v0
               (((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                  (Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
                  ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
                     T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
                     (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
                  (Integer -> Any
forall a b. a -> b
coe Integer
v0))
               Any
forall a. a
erased)
            Any
forall a. a
erased)
         ((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
            Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_3482
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> Integer -> Integer
mulInt
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
               (Integer -> Any
forall a b. a -> b
coe Integer
v1))))
-- Data.Nat.DivMod.m/n≤m
d_m'47'n'8804'm_452 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'47'n'8804'm_452 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22
d_m'47'n'8804'm_452 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> T__'8804'__22
du_m'47'n'8804'm_452 Integer
v0 Integer
v1
du_m'47'n'8804'm_452 ::
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'47'n'8804'm_452 :: Integer -> Integer -> T__'8804'__22
du_m'47'n'8804'm_452 Integer
v0 Integer
v1
  = (Integer -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
      Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'42''45'cancel'691''45''8804'_4030
      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
-- Data.Nat.DivMod.m/n<m
d_m'47'n'60'm_466 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'47'n'60'm_466 :: Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
d_m'47'n'60'm_466 Integer
v0 Integer
v1 ~T_NonZero_112
v2 ~T_NonZero_112
v3 ~T__'8804'__22
v4 = Integer -> Integer -> T__'8804'__22
du_m'47'n'60'm_466 Integer
v0 Integer
v1
du_m'47'n'60'm_466 ::
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'47'n'60'm_466 :: Integer -> Integer -> T__'8804'__22
du_m'47'n'60'm_466 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
      Integer -> Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'42''45'cancel'691''45''60'_4192
      (Integer -> Any
forall a b. a -> b
coe Integer
v1)
      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
      (Integer -> Any
forall a b. a -> b
coe Integer
v0)
-- Data.Nat.DivMod./-mono-≤
d_'47''45'mono'45''8804'_478 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_'47''45'mono'45''8804'_478 :: Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
d_'47''45'mono'45''8804'_478 Integer
v0 Integer
v1 Integer
v2 Integer
v3 ~T_NonZero_112
v4 ~T_NonZero_112
v5 T__'8804'__22
v6 T__'8804'__22
v7
  = Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
du_'47''45'mono'45''8804'_478 Integer
v0 Integer
v1 Integer
v2 Integer
v3 T__'8804'__22
v6 T__'8804'__22
v7
du_'47''45'mono'45''8804'_478 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_'47''45'mono'45''8804'_478 :: Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
du_'47''45'mono'45''8804'_478 Integer
v0 Integer
v1 Integer
v2 Integer
v3 T__'8804'__22
v4 T__'8804'__22
v5
  = case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v5 of
      MAlonzo.Code.Data.Nat.Base.C_s'8804's_34 T__'8804'__22
v8
        -> let v9 :: Integer
v9 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T__'8804'__22
forall a b. a -> b
coe
             (let v10 :: Integer
v10 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
              Any -> Any
forall a b. a -> b
coe
                ((Integer
 -> Integer
 -> Integer
 -> Integer
 -> Integer
 -> Integer
 -> T__'8804'__22
 -> T__'8804'__22
 -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                   Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
MAlonzo.Code.Data.Nat.DivMod.Core.d_div'8341''45'mono'45''8804'_886
                   (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3)
                   (Integer -> Any
forall a b. a -> b
coe Integer
v9) (Integer -> Any
forall a b. a -> b
coe Integer
v10) (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v4) (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v8)))
      T__'8804'__22
_ -> T__'8804'__22
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.DivMod./-monoˡ-≤
d_'47''45'mono'737''45''8804'_488 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_'47''45'mono'737''45''8804'_488 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
d_'47''45'mono'737''45''8804'_488 Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 T__'8804'__22
v4
  = Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_'47''45'mono'737''45''8804'_488 Integer
v0 Integer
v1 Integer
v2 T__'8804'__22
v4
du_'47''45'mono'737''45''8804'_488 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_'47''45'mono'737''45''8804'_488 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_'47''45'mono'737''45''8804'_488 Integer
v0 Integer
v1 Integer
v2 T__'8804'__22
v3
  = (Integer
 -> Integer
 -> Integer
 -> Integer
 -> T__'8804'__22
 -> T__'8804'__22
 -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
      Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
du_'47''45'mono'45''8804'_478 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
      (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v3)
      ((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
         Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'refl_2776 (Integer -> Any
forall a b. a -> b
coe Integer
v2))
-- Data.Nat.DivMod./-monoʳ-≤
d_'47''45'mono'691''45''8804'_504 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_'47''45'mono'691''45''8804'_504 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
d_'47''45'mono'691''45''8804'_504 Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 ~T_NonZero_112
v4 T__'8804'__22
v5
  = Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_'47''45'mono'691''45''8804'_504 Integer
v0 Integer
v1 Integer
v2 T__'8804'__22
v5
du_'47''45'mono'691''45''8804'_504 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_'47''45'mono'691''45''8804'_504 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_'47''45'mono'691''45''8804'_504 Integer
v0 Integer
v1 Integer
v2 T__'8804'__22
v3
  = (Integer
 -> Integer
 -> Integer
 -> Integer
 -> T__'8804'__22
 -> T__'8804'__22
 -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
      Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
du_'47''45'mono'45''8804'_478 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
      ((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
         Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'refl_2776 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
      (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v3)
-- Data.Nat.DivMod./-cancelʳ-≡
d_'47''45'cancel'691''45''8801'_518 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'47''45'cancel'691''45''8801'_518 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
-> T__'8801'__12
-> T__'8801'__12
d_'47''45'cancel'691''45''8801'_518 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m<n⇒m/n≡0
d_m'60'n'8658'm'47'n'8801'0_540 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'60'n'8658'm'47'n'8801'0_540 :: Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
d_m'60'n'8658'm'47'n'8801'0_540 = Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m≥n⇒m/n>0
d_m'8805'n'8658'm'47'n'62'0_554 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'8805'n'8658'm'47'n'62'0_554 :: Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8804'__22
d_m'8805'n'8658'm'47'n'62'0_554 Integer
v0 Integer
v1 ~T_NonZero_112
v2 T__'8804'__22
v3
  = Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_m'8805'n'8658'm'47'n'62'0_554 Integer
v0 Integer
v1 T__'8804'__22
v3
du_m'8805'n'8658'm'47'n'62'0_554 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'8805'n'8658'm'47'n'62'0_554 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_m'8805'n'8658'm'47'n'62'0_554 Integer
v0 Integer
v1 T__'8804'__22
v2
  = ((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
      (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> T__IsRelatedTo__78
 -> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
         (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
         (\ Any
v3 Any
v4 Any
v5 ->
            (T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854 Any
v5))
      (Integer
1 :: Integer)
      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
      (((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
         (\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 -> Any
v7) (Integer
1 :: Integer)
         ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
         ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
         (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
            (Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
            ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> Any -> (Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
               T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
               (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
               (\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 ->
                  (T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
                    T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986 Any
v6
                    Any
v7))
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
            (((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
               (Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
               ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
                  T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
                  (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
            ((Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_'47''45'mono'691''45''8804'_504 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
               (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v2)))
         Any
forall a. a
erased)
-- Data.Nat.DivMod.m/n≡0⇒m<n
d_m'47'n'8801'0'8658'm'60'n_568 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'47'n'8801'0'8658'm'60'n_568 :: Integer
-> Integer -> T_NonZero_112 -> T__'8801'__12 -> T__'8804'__22
d_m'47'n'8801'0'8658'm'60'n_568 Integer
v0 Integer
v1 ~T_NonZero_112
v2 ~T__'8801'__12
v3
  = Integer -> Integer -> T__'8804'__22
du_m'47'n'8801'0'8658'm'60'n_568 Integer
v0 Integer
v1
du_m'47'n'8801'0'8658'm'60'n_568 ::
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'47'n'8801'0'8658'm'60'n_568 :: Integer -> Integer -> T__'8804'__22
du_m'47'n'8801'0'8658'm'60'n_568 Integer
v0 Integer
v1
  = let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
    Any -> T__'8804'__22
forall a b. a -> b
coe
      (let v3 :: t
v3
             = (T__'8846'__30 -> T__'8846'__30) -> Any -> t
forall a b. a -> b
coe
                 T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_swap_78
                 (let v3 :: t
v3
                        = ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> (Any -> Any) -> Any -> Any -> t
forall a b. a -> b
coe
                            (Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                            (\ Any
v3 ->
                               (Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
                                 Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''7495''8658''8804'_2746
                                 (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                            ((T__'8804'__22 -> Any) -> Any
forall a b. a -> b
coe
                               T__'8804'__22 -> Any
MAlonzo.Code.Data.Nat.Properties.du_'8804''8658''8804''7495'_2758)
                            ((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                               Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                               ((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Bool
ltInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                               ((Bool -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
                                  Bool -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.d_T'45'reflects_66
                                  ((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Bool
ltInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v0)))) in
                  Any -> Any
forall a b. a -> b
coe
                    (case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v3 of
                       MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
                         -> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
                              then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
                                     MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v6
                                       -> (Any -> T__'8846'__30) -> Any -> Any
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (Any -> Any
forall a b. a -> b
coe Any
v6)
                                     T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                              else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                     Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v5)
                                     ((Any -> T__'8846'__30) -> Any -> Any
forall a b. a -> b
coe
                                        Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
                                        ((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
                                           Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8816''8658''62'_2888
                                           (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0)))
                       T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
       Any -> Any
forall a b. a -> b
coe
         (case Any -> T__'8846'__30
forall a b. a -> b
coe Any
forall a. a
v3 of
            MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v4 -> Any -> Any
forall a b. a -> b
coe Any
v4
            MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v4
              -> ((Any -> T_Irrelevant_20) -> Any) -> Any -> Any
forall a b. a -> b
coe
                   (Any -> T_Irrelevant_20) -> Any
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                   Any
forall a. a
erased
            T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
-- Data.Nat.DivMod.m/n≢0⇒n≤m
d_m'47'n'8802'0'8658'n'8804'm_608 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'47'n'8802'0'8658'n'8804'm_608 :: Integer
-> Integer
-> T_NonZero_112
-> (T__'8801'__12 -> T_Irrelevant_20)
-> T__'8804'__22
d_m'47'n'8802'0'8658'n'8804'm_608 Integer
v0 Integer
v1 ~T_NonZero_112
v2 ~T__'8801'__12 -> T_Irrelevant_20
v3
  = Integer -> Integer -> T__'8804'__22
du_m'47'n'8802'0'8658'n'8804'm_608 Integer
v0 Integer
v1
du_m'47'n'8802'0'8658'n'8804'm_608 ::
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'47'n'8802'0'8658'n'8804'm_608 :: Integer -> Integer -> T__'8804'__22
du_m'47'n'8802'0'8658'n'8804'm_608 Integer
v0 Integer
v1
  = let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
    Any -> T__'8804'__22
forall a b. a -> b
coe
      (let v3 :: t
v3
             = (T__'8846'__30 -> T__'8846'__30) -> Any -> t
forall a b. a -> b
coe
                 T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_swap_78
                 (let v3 :: t
v3
                        = ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> (Any -> Any) -> Any -> Any -> t
forall a b. a -> b
coe
                            (Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                            (\ Any
v3 ->
                               (Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
                                 Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''7495''8658''8804'_2746
                                 (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                            ((T__'8804'__22 -> Any) -> Any
forall a b. a -> b
coe
                               T__'8804'__22 -> Any
MAlonzo.Code.Data.Nat.Properties.du_'8804''8658''8804''7495'_2758)
                            ((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                               Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                               ((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Bool
ltInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                               ((Bool -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
                                  Bool -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.d_T'45'reflects_66
                                  ((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Bool
ltInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v0)))) in
                  Any -> Any
forall a b. a -> b
coe
                    (case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v3 of
                       MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
                         -> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
                              then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
                                     MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v6
                                       -> (Any -> T__'8846'__30) -> Any -> Any
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (Any -> Any
forall a b. a -> b
coe Any
v6)
                                     T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                              else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                     Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v5)
                                     ((Any -> T__'8846'__30) -> Any -> Any
forall a b. a -> b
coe
                                        Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
                                        ((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
                                           Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8816''8658''62'_2888
                                           (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0)))
                       T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
       Any -> Any
forall a b. a -> b
coe
         (case Any -> T__'8846'__30
forall a b. a -> b
coe Any
forall a. a
v3 of
            MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v4
              -> ((Any -> T_Irrelevant_20) -> Any) -> Any -> Any
forall a b. a -> b
coe
                   (Any -> T_Irrelevant_20) -> Any
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                   Any
forall a. a
erased
            MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v4 -> Any -> Any
forall a b. a -> b
coe Any
v4
            T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
-- Data.Nat.DivMod.+-distrib-/
d_'43''45'distrib'45''47'_644 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'43''45'distrib'45''47'_644 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8801'__12
d_'43''45'distrib'45''47'_644 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.+-distrib-/-∣ˡ
d_'43''45'distrib'45''47''45''8739''737'_662 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'43''45'distrib'45''47''45''8739''737'_662 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
d_'43''45'distrib'45''47''45''8739''737'_662 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.+-distrib-/-∣ʳ
d_'43''45'distrib'45''47''45''8739''691'_682 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'43''45'distrib'45''47''45''8739''691'_682 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
d_'43''45'distrib'45''47''45''8739''691'_682 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m/n≡1+[m∸n]/n
d_m'47'n'8801'1'43''91'm'8760'n'93''47'n_700 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'47'n'8801'1'43''91'm'8760'n'93''47'n_700 :: Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
d_m'47'n'8801'1'43''91'm'8760'n'93''47'n_700 = Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.[m∸n]/n≡m/n∸1
d_'91'm'8760'n'93''47'n'8801'm'47'n'8760'1_718 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'91'm'8760'n'93''47'n'8801'm'47'n'8760'1_718 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_'91'm'8760'n'93''47'n'8801'm'47'n'8760'1_718 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m∣n⇒o%n%m≡o%m
d_m'8739'n'8658'o'37'n'37'm'8801'o'37'm_750 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'8739'n'8658'o'37'n'37'm'8801'o'37'm_750 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
d_m'8739'n'8658'o'37'n'37'm'8801'o'37'm_750 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod._.pm
d_pm_764 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_pm_764 :: Integer
-> Integer -> T_NonZero_112 -> Integer -> T_NonZero_112 -> Integer
d_pm_764 Integer
v0 ~Integer
v1 ~T_NonZero_112
v2 Integer
v3 ~T_NonZero_112
v4 = Integer -> Integer -> Integer
du_pm_764 Integer
v0 Integer
v3
du_pm_764 :: Integer -> Integer -> Integer
du_pm_764 :: Integer -> Integer -> Integer
du_pm_764 Integer
v0 Integer
v1 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
-- Data.Nat.DivMod._.lem
d_lem_766 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_lem_766 :: Integer
-> Integer
-> T_NonZero_112
-> Integer
-> T_NonZero_112
-> T__'8804'__22
d_lem_766 Integer
v0 Integer
v1 ~T_NonZero_112
v2 Integer
v3 ~T_NonZero_112
v4 = Integer -> Integer -> Integer -> T__'8804'__22
du_lem_766 Integer
v0 Integer
v1 Integer
v3
du_lem_766 ::
  Integer ->
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_lem_766 :: Integer -> Integer -> Integer -> T__'8804'__22
du_lem_766 Integer
v0 Integer
v1 Integer
v2
  = ((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> T__'8804'__22
forall a b. a -> b
coe
      (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> T__IsRelatedTo__78
 -> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
         (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
         (\ Any
v3 Any
v4 Any
v5 ->
            (T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854 Any
v5))
      (Integer -> Integer -> Integer
mulInt
         ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
            Integer -> Integer -> Integer
mulInt
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v1)
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pm_764 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
            (Integer -> Any
forall a b. a -> b
coe Integer
v2))
         (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
      Integer
v1
      (((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
         (\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 -> Any
v7)
         (Integer -> Integer -> Integer
mulInt
            ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
               Integer -> Integer -> Integer
mulInt
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                  Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v1)
                  ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pm_764 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
               (Integer -> Any
forall a b. a -> b
coe Integer
v2))
            (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
         (Integer -> Integer -> Integer
mulInt
            ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
               Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v1)
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pm_764 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
            ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pm_764 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
         Integer
v1
         (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
            (Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
            ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> Any -> (Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
               T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
               (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
               (\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 ->
                  (T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
                    T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986 Any
v6
                    Any
v7))
            (Integer -> Integer -> Integer
mulInt
               ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
                  Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v1)
                  ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pm_764 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
               ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pm_764 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
            Integer
v1 Integer
v1
            (((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
               (Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
               ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
                  T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
                  (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
               (Integer -> Any
forall a b. a -> b
coe Integer
v1))
            ((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> Integer -> T__'8804'__22
du_m'47'n'42'n'8804'm_440 (Integer -> Any
forall a b. a -> b
coe Integer
v1)
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pm_764 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2))))
         Any
forall a. a
erased)
-- Data.Nat.DivMod.m*n/m*o≡n/o
d_m'42'n'47'm'42'o'8801'n'47'o_780 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'42'n'47'm'42'o'8801'n'47'o_780 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
d_m'42'n'47'm'42'o'8801'n'47'o_780 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod._.helper
d_helper_796 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  Integer ->
  MAlonzo.Code.Induction.WellFounded.T_Acc_42 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_helper_796 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> Integer
-> T_Acc_42
-> T__'8801'__12
d_helper_796 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> Integer
-> T_Acc_42
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod._._.n∸o<n
d_n'8760'o'60'n_828 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  (Integer ->
   MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
   MAlonzo.Code.Induction.WellFounded.T_Acc_42) ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_n'8760'o'60'n_828 :: Integer
-> Integer
-> T__'8804'__22
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> (Integer -> T__'8804'__22 -> T_Acc_42)
-> T__'8804'__22
d_n'8760'o'60'n_828 Integer
v0 Integer
v1 T__'8804'__22
v2 ~Integer
v3 ~Integer
v4 ~T_NonZero_112
v5 ~T_NonZero_112
v6 ~Integer -> T__'8804'__22 -> T_Acc_42
v7
  = Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_n'8760'o'60'n_828 Integer
v0 Integer
v1 T__'8804'__22
v2
du_n'8760'o'60'n_828 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_n'8760'o'60'n_828 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_n'8760'o'60'n_828 Integer
v0 Integer
v1 T__'8804'__22
v2
  = (Integer
 -> Integer
 -> Integer
 -> T__'8804'__22
 -> T__'8804'__22
 -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
      Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_'8760''45'mono'691''45''60'_5134
      (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
      ((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
         Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_n'8802'0'8658'n'62'0_3090
         (Integer -> Any
forall a b. a -> b
coe Integer
v0))
      (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v2)
-- Data.Nat.DivMod.m*n/o*n≡m/o
d_m'42'n'47'o'42'n'8801'm'47'o_842 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'42'n'47'o'42'n'8801'm'47'o_842 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
d_m'42'n'47'o'42'n'8801'm'47'o_842 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m<n*o⇒m/o<n
d_m'60'n'42'o'8658'm'47'o'60'n_866 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'60'n'42'o'8658'm'47'o'60'n_866 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
d_m'60'n'42'o'8658'm'47'o'60'n_866 Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 ~T__'8804'__22
v4
  = Integer -> Integer -> Integer -> T__'8804'__22
du_m'60'n'42'o'8658'm'47'o'60'n_866 Integer
v0 Integer
v1 Integer
v2
du_m'60'n'42'o'8658'm'47'o'60'n_866 ::
  Integer ->
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'60'n'42'o'8658'm'47'o'60'n_866 :: Integer -> Integer -> Integer -> T__'8804'__22
du_m'60'n'42'o'8658'm'47'o'60'n_866 Integer
v0 Integer
v1 Integer
v2
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
1 -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v2) in
           Any -> T__'8804'__22
forall a b. a -> b
coe
             (let v4 :: b
v4
                    = T_SubRelation_60 -> b
forall a b. a -> b
coe
                        T_SubRelation_60
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_strictRelation_202 in
              Any -> Any
forall a b. a -> b
coe
                ((T_SubRelation_60 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                   T_SubRelation_60 -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__126
                   (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4)
                   ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v3))
                   (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                   (((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                      (Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
                      (\ Any
v5 Any
v6 Any
v7 Any
v8 Any
v9 -> Any
v9)
                      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v3))
                      (Integer
0 :: Integer) (Integer
1 :: Integer)
                      (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
                         (Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''60'_312
                         (((Any -> Any -> Any -> Any -> Any -> Any)
 -> T_Σ_14
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
forall a b. a -> b
coe
                            (Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'60''45'go_152
                            (\ Any
v5 Any
v6 Any
v7 Any
v8 Any
v9 ->
                               (Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                 Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans_2980 Any
v6 Any
v8 Any
v9)
                            (T_Σ_14 -> Any
forall a b. a -> b
coe
                               T_Σ_14
MAlonzo.Code.Relation.Binary.PropositionalEquality.Core.du_resp'8322'_160)
                            (\ Any
v5 Any
v6 Any
v7 Any
v8 Any
v9 ->
                               (T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                 T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45''8804''45'trans_2992 Any
v8
                                 Any
v9))
                         (Integer
0 :: Integer) (Integer
1 :: Integer) (Integer
1 :: Integer)
                         (((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                            (Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
                            ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
                               T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
                               (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
                            (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)))
                         ((T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
                            T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Base.C_s'8804's_34
                            (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_26)))
                      Any
forall a. a
erased)))
      Integer
_ -> (Integer -> Integer -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Integer -> Any -> T__'8804'__22
forall a b. a -> b
coe
             Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_pred'45'cancel'45''60'_5686
             ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)) Integer
v1
             (let v3 :: b
v3
                    = T_SubRelation_60 -> b
forall a b. a -> b
coe
                        T_SubRelation_60
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_strictRelation_202 in
              Any -> Any
forall a b. a -> b
coe
                ((T_SubRelation_60 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                   T_SubRelation_60 -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__126
                   (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v3)
                   ((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe
                      Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d_pred_192
                      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
                   ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)))
                   (((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Any
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                      (Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
                      (\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 -> Any
v8)
                      (Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d_pred_192
                         ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
                      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                         Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314
                         ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v0 Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
                      (Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)))
                      (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
                         (Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''60'_312
                         (((Any -> Any -> Any -> Any -> Any -> Any)
 -> T_Σ_14
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
forall a b. a -> b
coe
                            (Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'60''45'go_152
                            (\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
                               (Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                 Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans_2980 Any
v5 Any
v7 Any
v8)
                            (T_Σ_14 -> Any
forall a b. a -> b
coe
                               T_Σ_14
MAlonzo.Code.Relation.Binary.PropositionalEquality.Core.du_resp'8322'_160)
                            (\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
                               (T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                 T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45''8804''45'trans_2992 Any
v7
                                 Any
v8))
                         ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                            Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314
                            ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v0 Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
                         (Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)))
                         (Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)))
                         (((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                            (Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
                            ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
                               T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
                               (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
                            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))))
                         ((Integer -> Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                            Integer -> Integer -> Integer -> T__'8804'__22
du_m'60'n'42'o'8658'm'47'o'60'n_866
                            ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v0 Integer
v2)
                            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
                      Any
forall a. a
erased)))
-- Data.Nat.DivMod.[m∸n*o]/o≡m/o∸n
d_'91'm'8760'n'42'o'93''47'o'8801'm'47'o'8760'n_900 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'91'm'8760'n'42'o'93''47'o'8801'm'47'o'8760'n_900 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_'91'm'8760'n'42'o'93''47'o'8801'm'47'o'8760'n_900 = Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m/n/o≡m/[n*o]
d_m'47'n'47'o'8801'm'47''91'n'42'o'93'_926 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'47'n'47'o'8801'm'47''91'n'42'o'93'_926 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
d_m'47'n'47'o'8801'm'47''91'n'42'o'93'_926 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod._.n*o
d_n'42'o_938 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_n'42'o_938 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> Integer
d_n'42'o_938 ~Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 ~T_NonZero_112
v4 ~T_NonZero_112
v5 = Integer -> Integer -> Integer
du_n'42'o_938 Integer
v1 Integer
v2
du_n'42'o_938 :: Integer -> Integer -> Integer
du_n'42'o_938 :: Integer -> Integer -> Integer
du_n'42'o_938 Integer
v0 Integer
v1 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Nat.DivMod._.o*n
d_o'42'n_940 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_o'42'n_940 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> Integer
d_o'42'n_940 ~Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 ~T_NonZero_112
v4 ~T_NonZero_112
v5 = Integer -> Integer -> Integer
du_o'42'n_940 Integer
v1 Integer
v2
du_o'42'n_940 :: Integer -> Integer -> Integer
du_o'42'n_940 :: Integer -> Integer -> Integer
du_o'42'n_940 Integer
v0 Integer
v1 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
-- Data.Nat.DivMod._.lem₁
d_lem'8321'_942 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_lem'8321'_942 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8739'__20
d_lem'8321'_942 Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 ~T_NonZero_112
v4 ~T_NonZero_112
v5 = Integer -> Integer -> Integer -> T__'8739'__20
du_lem'8321'_942 Integer
v0 Integer
v1 Integer
v2
du_lem'8321'_942 ::
  Integer ->
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_lem'8321'_942 :: Integer -> Integer -> Integer -> T__'8739'__20
du_lem'8321'_942 Integer
v0 Integer
v1 Integer
v2
  = (Integer -> T__'8739'__20) -> Integer -> T__'8739'__20
forall a b. a -> b
coe
      Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34
      (Integer -> Integer -> Integer
mulInt
         ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
            Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_n'42'o_938 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
         (Integer -> Integer
forall a b. a -> b
coe Integer
v2))
-- Data.Nat.DivMod._.lem₂
d_lem'8322'_946 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lem'8322'_946 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
d_lem'8322'_946 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod._.lem₃
d_lem'8323'_950 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_lem'8323'_950 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8804'__22
d_lem'8323'_950 Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 ~T_NonZero_112
v4 ~T_NonZero_112
v5 = Integer -> Integer -> Integer -> T__'8804'__22
du_lem'8323'_950 Integer
v0 Integer
v1 Integer
v2
du_lem'8323'_950 ::
  Integer ->
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_lem'8323'_950 :: Integer -> Integer -> Integer -> T__'8804'__22
du_lem'8323'_950 Integer
v0 Integer
v1 Integer
v2
  = let v3 :: b
v3
          = T_SubRelation_60 -> b
forall a b. a -> b
coe
              T_SubRelation_60
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_strictRelation_202 in
    Any -> T__'8804'__22
forall a b. a -> b
coe
      ((T_SubRelation_60 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
         T_SubRelation_60 -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__126
         (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v3)
         ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
            Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_n'42'o_938 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
         ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_o'42'n_940 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
         (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
            (Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''60'_312
            (((Any -> Any -> Any -> Any -> Any -> Any)
 -> T_Σ_14
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
forall a b. a -> b
coe
               (Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'60''45'go_152
               (\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
                  (Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                    Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans_2980 Any
v5 Any
v7 Any
v8)
               (T_Σ_14 -> Any
forall a b. a -> b
coe
                  T_Σ_14
MAlonzo.Code.Relation.Binary.PropositionalEquality.Core.du_resp'8322'_160)
               (\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
                  (T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
                    T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45''8804''45'trans_2992 Any
v7
                    Any
v8))
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_n'42'o_938 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_n'42'o_938 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_o'42'n_940 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
            (((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
               (Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
               (\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 -> Any
v8) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_n'42'o_938 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_o'42'n_940 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_o'42'n_940 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
               (((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                  (Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
                  ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
                     T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
                     (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
                  ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_o'42'n_940 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
               Any
forall a. a
erased)
            ((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> Integer -> T__'8804'__22
du_m'37'n'60'n_166 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_n'42'o_938 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))))
-- Data.Nat.DivMod.*-/-assoc
d_'42''45''47''45'assoc_966 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'42''45''47''45'assoc_966 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
d_'42''45''47''45'assoc_966 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod./-*-interchange
d_'47''45''42''45'interchange_988 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'47''45''42''45'interchange_988 :: Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
-> T__'8801'__12
d_'47''45''42''45'interchange_988 = Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m*n/m!≡n/[m∸1]!
d_m'42'n'47'm'33''8801'n'47''91'm'8760'1'93''33'_1012 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'42'n'47'm'33''8801'n'47''91'm'8760'1'93''33'_1012 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_m'42'n'47'm'33''8801'n'47''91'm'8760'1'93''33'_1012 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m%[n*o]/o≡m/o%n
d_m'37''91'n'42'o'93''47'o'8801'm'47'o'37'n_1040 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'37''91'n'42'o'93''47'o'8801'm'47'o'37'n_1040 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
d_m'37''91'n'42'o'93''47'o'8801'm'47'o'37'n_1040 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.m%n*o≡m*o%[n*o]
d_m'37'n'42'o'8801'm'42'o'37''91'n'42'o'93'_1070 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'37'n'42'o'8801'm'42'o'37''91'n'42'o'93'_1070 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
d_m'37'n'42'o'8801'm'42'o'37''91'n'42'o'93'_1070 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.[m*n+o]%[p*n]≡[m*n]%[p*n]+o
d_'91'm'42'n'43'o'93''37''91'p'42'n'93''8801''91'm'42'n'93''37''91'p'42'n'93''43'o_1094 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'91'm'42'n'43'o'93''37''91'p'42'n'93''8801''91'm'42'n'93''37''91'p'42'n'93''43'o_1094 :: Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8801'__12
d_'91'm'42'n'43'o'93''37''91'p'42'n'93''8801''91'm'42'n'93''37''91'p'42'n'93''43'o_1094
  = Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod._.mn
d_mn_1112 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 -> Integer
d_mn_1112 :: Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> Integer
d_mn_1112 Integer
v0 Integer
v1 ~Integer
v2 ~Integer
v3 ~T_NonZero_112
v4 ~T__'8804'__22
v5 = Integer -> Integer -> Integer
du_mn_1112 Integer
v0 Integer
v1
du_mn_1112 :: Integer -> Integer -> Integer
du_mn_1112 :: Integer -> Integer -> Integer
du_mn_1112 Integer
v0 Integer
v1 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Nat.DivMod._.pn
d_pn_1114 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 -> Integer
d_pn_1114 :: Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> Integer
d_pn_1114 ~Integer
v0 Integer
v1 ~Integer
v2 Integer
v3 ~T_NonZero_112
v4 ~T__'8804'__22
v5 = Integer -> Integer -> Integer
du_pn_1114 Integer
v1 Integer
v3
du_pn_1114 :: Integer -> Integer -> Integer
du_pn_1114 :: Integer -> Integer -> Integer
du_pn_1114 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
-- Data.Nat.DivMod._.lem₁
d_lem'8321'_1116 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_lem'8321'_1116 :: Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
d_lem'8321'_1116 Integer
v0 Integer
v1 ~Integer
v2 Integer
v3 ~T_NonZero_112
v4 ~T__'8804'__22
v5 = Integer -> Integer -> Integer -> T__'8804'__22
du_lem'8321'_1116 Integer
v0 Integer
v1 Integer
v3
du_lem'8321'_1116 ::
  Integer ->
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_lem'8321'_1116 :: Integer -> Integer -> Integer -> T__'8804'__22
du_lem'8321'_1116 Integer
v0 Integer
v1 Integer
v2
  = ((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Any -> Integer -> Any -> T__'8804'__22
forall a b. a -> b
coe
      (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> T__IsRelatedTo__78
 -> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
         (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
         (\ Any
v3 Any
v4 Any
v5 ->
            (T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854 Any
v5))
      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
         Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326
         ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_mn_1112 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
         ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
      (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
      (((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
         (\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 -> Any
v7)
         ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
            Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_mn_1112 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
         (Integer -> Integer -> Integer
mulInt
            ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
               Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
            (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
         (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
         (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
            (Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
            ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> Any -> (Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
               T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
               (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
               (\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 ->
                  (T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
                    T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986 Any
v6
                    Any
v7))
            (Integer -> Integer -> Integer
mulInt
               ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
                  Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
                  ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
               (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
            (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
            (((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
               (Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
               ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
                  T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
                  (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
            ((Integer -> Integer -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'42''45'mono'737''45''8804'_4070
               (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)
               ((T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
                  T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'60'1'43'n'8658'm'8804'n_3122
                  ((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
                     Integer -> Integer -> T__'8804'__22
du_m'37'n'60'n_166 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
                     ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v2))))))
         Any
forall a. a
erased)
-- Data.Nat.DivMod._.lem₂
d_lem'8322'_1118 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_lem'8322'_1118 :: Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
d_lem'8322'_1118 Integer
v0 Integer
v1 Integer
v2 Integer
v3 ~T_NonZero_112
v4 T__'8804'__22
v5
  = Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_lem'8322'_1118 Integer
v0 Integer
v1 Integer
v2 Integer
v3 T__'8804'__22
v5
du_lem'8322'_1118 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_lem'8322'_1118 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_lem'8322'_1118 Integer
v0 Integer
v1 Integer
v2 Integer
v3 T__'8804'__22
v4
  = let v5 :: b
v5
          = T_SubRelation_60 -> b
forall a b. a -> b
coe
              T_SubRelation_60
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_strictRelation_202 in
    Any -> T__'8804'__22
forall a b. a -> b
coe
      ((T_SubRelation_60 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
         T_SubRelation_60 -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__126
         (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v5)
         ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
            Integer -> Integer -> Integer
addInt
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_mn_1112 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3)))
            (Integer -> Any
forall a b. a -> b
coe Integer
v2))
         ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3))
         (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
            (Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''60'_312
            (((Any -> Any -> Any -> Any -> Any -> Any)
 -> T_Σ_14
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
forall a b. a -> b
coe
               (Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'60''45'go_152
               (\ Any
v6 Any
v7 Any
v8 Any
v9 Any
v10 ->
                  (Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                    Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans_2980 Any
v7 Any
v9 Any
v10)
               (T_Σ_14 -> Any
forall a b. a -> b
coe
                  T_Σ_14
MAlonzo.Code.Relation.Binary.PropositionalEquality.Core.du_resp'8322'_160)
               (\ Any
v6 Any
v7 Any
v8 Any
v9 Any
v10 ->
                  (T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
                    T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45''8804''45'trans_2992 Any
v9
                    Any
v10))
            (Integer -> Integer -> Integer
addInt
               ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
                  Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326
                  ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_mn_1112 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                  ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3)))
               (Integer -> Integer
forall a b. a -> b
coe Integer
v2))
            (Integer -> Integer -> Integer
addInt ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v1)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3))
            (((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
               (Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
               (\ Any
v6 Any
v7 Any
v8 Any
v9 Any
v10 -> Any
v10)
               (Integer -> Integer -> Integer
addInt ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v1)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3))
               ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3))
               (((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                  (Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
                  ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
                     T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
                     (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
                  ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3)))
               Any
forall a. a
erased)
            ((Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'43''45'mono'45''8804''45''60'_3570
               (Integer -> Any
forall a b. a -> b
coe Integer
v1) ((Integer -> Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer -> T__'8804'__22
du_lem'8321'_1116 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3))
               (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v4))))
-- Data.Nat.DivMod.DivMod
d_DivMod_1126 :: p -> p -> ()
d_DivMod_1126 p
a0 p
a1 = ()
data T_DivMod_1126
  = C_result_1146 Integer MAlonzo.Code.Data.Fin.Base.T_Fin_10
-- Data.Nat.DivMod.DivMod.quotient
d_quotient_1138 :: T_DivMod_1126 -> Integer
d_quotient_1138 :: T_DivMod_1126 -> Integer
d_quotient_1138 T_DivMod_1126
v0
  = case T_DivMod_1126 -> T_DivMod_1126
forall a b. a -> b
coe T_DivMod_1126
v0 of
      C_result_1146 Integer
v1 T_Fin_10
v2 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      T_DivMod_1126
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.DivMod.DivMod.remainder
d_remainder_1140 ::
  T_DivMod_1126 -> MAlonzo.Code.Data.Fin.Base.T_Fin_10
d_remainder_1140 :: T_DivMod_1126 -> T_Fin_10
d_remainder_1140 T_DivMod_1126
v0
  = case T_DivMod_1126 -> T_DivMod_1126
forall a b. a -> b
coe T_DivMod_1126
v0 of
      C_result_1146 Integer
v1 T_Fin_10
v2 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v2
      T_DivMod_1126
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.DivMod.DivMod.property
d_property_1142 ::
  T_DivMod_1126 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_property_1142 :: T_DivMod_1126 -> T__'8801'__12
d_property_1142 = T_DivMod_1126 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.DivMod.nonZeroDivisor
d_nonZeroDivisor_1144 ::
  Integer ->
  Integer ->
  T_DivMod_1126 -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112
d_nonZeroDivisor_1144 :: Integer -> Integer -> T_DivMod_1126 -> T_NonZero_112
d_nonZeroDivisor_1144 ~Integer
v0 ~Integer
v1 ~T_DivMod_1126
v2 = T_NonZero_112
du_nonZeroDivisor_1144
du_nonZeroDivisor_1144 :: MAlonzo.Code.Data.Nat.Base.T_NonZero_112
du_nonZeroDivisor_1144 :: T_NonZero_112
du_nonZeroDivisor_1144
  = T_NonZero_112 -> T_NonZero_112
forall a b. a -> b
coe T_NonZero_112
MAlonzo.Code.Data.Fin.Properties.du_nonZeroIndex_22
-- Data.Nat.DivMod._div_
d__div__1154 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d__div__1154 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__div__1154 Integer
v0 Integer
v1 T_NonZero_112
v2
  = (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 Integer
v0 Integer
v1
-- Data.Nat.DivMod._mod_
d__mod__1162 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10
d__mod__1162 :: Integer -> Integer -> T_NonZero_112 -> T_Fin_10
d__mod__1162 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> T_Fin_10
du__mod__1162 Integer
v0 Integer
v1
du__mod__1162 ::
  Integer -> Integer -> MAlonzo.Code.Data.Fin.Base.T_Fin_10
du__mod__1162 :: Integer -> Integer -> T_Fin_10
du__mod__1162 Integer
v0 Integer
v1
  = (Integer -> T_Fin_10) -> Any -> T_Fin_10
forall a b. a -> b
coe
      Integer -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.du_fromℕ'60'_52
      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
-- Data.Nat.DivMod._divMod_
d__divMod__1174 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> T_DivMod_1126
d__divMod__1174 :: Integer -> Integer -> T_NonZero_112 -> T_DivMod_1126
d__divMod__1174 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> T_DivMod_1126
du__divMod__1174 Integer
v0 Integer
v1
du__divMod__1174 :: Integer -> Integer -> T_DivMod_1126
du__divMod__1174 :: Integer -> Integer -> T_DivMod_1126
du__divMod__1174 Integer
v0 Integer
v1
  = (Integer -> T_Fin_10 -> T_DivMod_1126)
-> Any -> Any -> T_DivMod_1126
forall a b. a -> b
coe
      Integer -> T_Fin_10 -> T_DivMod_1126
C_result_1146
      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
      ((Integer -> Integer -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T_Fin_10
du__mod__1162 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
-- Data.Nat.DivMod._.[m/n]*n
d_'91'm'47'n'93''42'n_1184 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_'91'm'47'n'93''42'n_1184 :: Integer -> Integer -> T_NonZero_112 -> Integer
d_'91'm'47'n'93''42'n_1184 Integer
v0 Integer
v1 ~T_NonZero_112
v2
  = Integer -> Integer -> Integer
du_'91'm'47'n'93''42'n_1184 Integer
v0 Integer
v1
du_'91'm'47'n'93''42'n_1184 :: Integer -> Integer -> Integer
du_'91'm'47'n'93''42'n_1184 :: Integer -> Integer -> Integer
du_'91'm'47'n'93''42'n_1184 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
      Integer -> Integer -> Integer
mulInt
      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
      (Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Nat.DivMod._.[m%n]<n
d_'91'm'37'n'93''60'n_1186 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_'91'm'37'n'93''60'n_1186 :: Integer
-> Integer -> T_NonZero_112 -> T_NonZero_112 -> T__'8804'__22
d_'91'm'37'n'93''60'n_1186 Integer
v0 Integer
v1 ~T_NonZero_112
v2
  = Integer -> Integer -> T_NonZero_112 -> T__'8804'__22
du_'91'm'37'n'93''60'n_1186 Integer
v0 Integer
v1
du_'91'm'37'n'93''60'n_1186 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_'91'm'37'n'93''60'n_1186 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22
du_'91'm'37'n'93''60'n_1186 Integer
v0 Integer
v1 T_NonZero_112
v2
  = (Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe Integer -> Integer -> T__'8804'__22
du_m'37'n'60'n_166 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)