{-# 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.Core 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.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Data.Sum.Base
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

-- Data.Nat.DivMod.Core.mod-cong₃
d_mod'45'cong'8323'_18 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_mod'45'cong'8323'_18 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8801'__12
-> T__'8801'__12
d_mod'45'cong'8323'_18 = Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.modₕ-skipTo0
d_mod'8341''45'skipTo0_28 ::
  Integer ->
  Integer ->
  Integer ->
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_mod'8341''45'skipTo0_28 :: Integer -> Integer -> Integer -> Integer -> T__'8801'__12
d_mod'8341''45'skipTo0_28 = Integer -> Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.a[modₕ]1≡0
d_a'91'mod'8341''93'1'8801'0_50 ::
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_a'91'mod'8341''93'1'8801'0_50 :: Integer -> T__'8801'__12
d_a'91'mod'8341''93'1'8801'0_50 = Integer -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.n[modₕ]n≡0
d_n'91'mod'8341''93'n'8801'0_58 ::
  Integer ->
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_n'91'mod'8341''93'n'8801'0_58 :: Integer -> Integer -> T__'8801'__12
d_n'91'mod'8341''93'n'8801'0_58 = Integer -> Integer -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.a[modₕ]n<n
d_a'91'mod'8341''93'n'60'n_70 ::
  Integer ->
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_a'91'mod'8341''93'n'60'n_70 :: Integer -> Integer -> Integer -> T__'8804'__22
d_a'91'mod'8341''93'n'60'n_70 Integer
v0 Integer
v1 Integer
v2
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> (Integer -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
             Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_3482 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
      Integer
_ -> let v3 :: Integer
v3 = 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
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
                Integer
0 -> (Integer -> Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       Integer -> Integer -> Integer -> T__'8804'__22
d_a'91'mod'8341''93'n'60'n_70 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v3)
                       (Integer -> Any
forall a b. a -> b
coe Integer
v0)
                Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
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
d_a'91'mod'8341''93'n'60'n_70
                          ((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
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v4)))
-- Data.Nat.DivMod.Core.a[modₕ]n≤a
d_a'91'mod'8341''93'n'8804'a_96 ::
  Integer ->
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_a'91'mod'8341''93'n'8804'a_96 :: Integer -> Integer -> Integer -> T__'8804'__22
d_a'91'mod'8341''93'n'8804'a_96 Integer
v0 Integer
v1 Integer
v2
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> (Integer -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
             Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'reflexive_2772
             ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0
                (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v2)) (Integer
0 :: Integer) Integer
v2)
      Integer
_ -> let v3 :: Integer
v3 = 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
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
                Integer
0 -> ((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Any -> Integer -> Any -> Any
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
v4 Any
v5 Any
v6 ->
                             (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
v6))
                       ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0 Integer
v0 Integer
v1
                          (Integer
0 :: Integer))
                       (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (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
-> 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''10217'_436
                          (\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 -> Any
v8)
                          ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                             Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0 Integer
v0 Integer
v1
                             (Integer
0 :: Integer))
                          ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                             Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0 Integer
v0 Integer
v1
                             (Integer
0 :: Integer))
                          (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                          (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Integer -> Integer -> Any -> T__'8804'__22 -> 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
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_'8804''45''60''45'trans_2986
                                     Any
v7 Any
v8))
                             ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0 Integer
v0 Integer
v1
                                (Integer
0 :: Integer))
                             Integer
v3 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (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
-> T__'8804'__22
-> 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
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_'8804''45''60''45'trans_2986
                                        Any
v7 Any
v8))
                                Integer
v3 Integer
v1 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (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
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_'8804''45''60''45'trans_2986
                                           Any
v7 Any
v8))
                                   Integer
v1 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (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
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
                                   ((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
                                      Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'n'43'm_3494
                                      (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
                                (Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_2844 (Integer -> Integer
forall a b. a -> b
coe Integer
v3)))
                             (Integer -> Integer -> Integer -> T__'8804'__22
d_a'91'mod'8341''93'n'8804'a_96
                                (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)))
                          Any
forall a. a
erased)
                Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
forall a b. a -> b
coe
                       (((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Any -> Integer -> Any -> Any
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
v5 Any
v6 Any
v7 ->
                                (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
v7))
                          ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                             Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0
                             (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v2)) Integer
v1 Integer
v2)
                          (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (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
-> 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''10217'_436
                             (\ Any
v5 Any
v6 Any
v7 Any
v8 Any
v9 -> Any
v9)
                             ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0
                                (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v2)) Integer
v1 Integer
v2)
                             ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0
                                (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v2)) Integer
v1 Integer
v2)
                             (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                             (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Integer -> Integer -> Any -> T__'8804'__22 -> 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
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_'8804''45''60''45'trans_2986
                                        Any
v8 Any
v9))
                                ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                   Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0
                                   (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v2)) Integer
v1 Integer
v2)
                                (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (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)
-> 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
v5 Any
v6 Any
v7 Any
v8 Any
v9 -> Any
v9) (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                   (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (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
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
                                   Any
forall a. a
erased)
                                (Integer -> Integer -> Integer -> T__'8804'__22
d_a'91'mod'8341''93'n'8804'a_96
                                   ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
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
v0)) (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)))
                             Any
forall a. a
erased)))
-- Data.Nat.DivMod.Core.a≤n⇒a[modₕ]n≡a
d_a'8804'n'8658'a'91'mod'8341''93'n'8801'a_124 ::
  Integer ->
  Integer ->
  Integer ->
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_a'8804'n'8658'a'91'mod'8341''93'n'8801'a_124 :: Integer -> Integer -> Integer -> Integer -> T__'8801'__12
d_a'8804'n'8658'a'91'mod'8341''93'n'8801'a_124 = Integer -> Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.modₕ-idem
d_mod'8341''45'idem_146 ::
  Integer ->
  Integer ->
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_mod'8341''45'idem_146 :: Integer -> Integer -> Integer -> T__'8801'__12
d_mod'8341''45'idem_146 = Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.a+1[modₕ]n≡0⇒a[modₕ]n≡n-1
d_a'43'1'91'mod'8341''93'n'8801'0'8658'a'91'mod'8341''93'n'8801'n'45'1_176 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_a'43'1'91'mod'8341''93'n'8801'0'8658'a'91'mod'8341''93'n'8801'n'45'1_176 :: Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
d_a'43'1'91'mod'8341''93'n'8801'0'8658'a'91'mod'8341''93'n'8801'n'45'1_176
  = Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.k<1+a[modₕ]n⇒k≤a[modₕ]n
d_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
d_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 Integer
v0
                                                                    ~Integer
v1 Integer
v2 Integer
v3 T__'8804'__22
v4
  = Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216
      Integer
v0 Integer
v2 Integer
v3 T__'8804'__22
v4
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 Integer
v0
                                                                     Integer
v1 Integer
v2 T__'8804'__22
v3
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v3 of
             MAlonzo.Code.Data.Nat.Base.C_s'8804's_34 T__'8804'__22
v6 -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v6
             T__'8804'__22
_ -> T__'8804'__22
forall a. a
MAlonzo.RTE.mazUnreachableError
      Integer
_ -> let v4 :: Integer
v4 = 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
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
                Integer
0 -> (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_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
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v3)
                Integer
_ -> let v5 :: Integer
v5 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
forall a b. a -> b
coe
                       ((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_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216
                          ((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
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v5)
                          (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v3)))
-- Data.Nat.DivMod.Core.1+a[modₕ]n≤1+k⇒a[modₕ]n≤k
d_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 ::
  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
d_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 :: Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
d_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 Integer
v0
                                                                           ~Integer
v1 Integer
v2 Integer
v3 ~T__'8804'__22
v4 T__'8804'__22
v5
  = Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260
      Integer
v0 Integer
v2 Integer
v3 T__'8804'__22
v5
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 Integer
v0
                                                                            Integer
v1 Integer
v2 T__'8804'__22
v3
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v3 of
             MAlonzo.Code.Data.Nat.Base.C_s'8804's_34 T__'8804'__22
v6 -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v6
             T__'8804'__22
_ -> T__'8804'__22
forall a. a
MAlonzo.RTE.mazUnreachableError
      Integer
_ -> let v4 :: Integer
v4 = 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
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
                Integer
0 -> (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_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
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v3)
                Integer
_ -> let v5 :: Integer
v5 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
forall a b. a -> b
coe
                       ((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_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260
                          ((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
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v5)
                          (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v3)))
-- Data.Nat.DivMod.Core.a+n[modₕ]n≡a[modₕ]n
d_a'43'n'91'mod'8341''93'n'8801'a'91'mod'8341''93'n_308 ::
  Integer ->
  Integer ->
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_a'43'n'91'mod'8341''93'n'8801'a'91'mod'8341''93'n_308 :: Integer -> Integer -> Integer -> T__'8801'__12
d_a'43'n'91'mod'8341''93'n'8801'a'91'mod'8341''93'n_308 = Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core._.mod₁
d_mod'8321'_336 ::
  Integer -> Integer -> Integer -> Integer -> Integer -> Integer
d_mod'8321'_336 :: Integer -> Integer -> Integer -> Integer -> Integer -> Integer
d_mod'8321'_336 Integer
v0 Integer
v1 ~Integer
v2 = Integer -> Integer -> Integer -> Integer -> Integer
du_mod'8321'_336 Integer
v0 Integer
v1
du_mod'8321'_336 ::
  Integer -> Integer -> Integer -> Integer -> Integer
du_mod'8321'_336 :: Integer -> Integer -> Integer -> Integer -> Integer
du_mod'8321'_336 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Integer
forall a b. a -> b
coe
      Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0
      (Integer -> Integer -> Integer
addInt ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
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
v0)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
-- Data.Nat.DivMod.Core._.mod₂
d_mod'8322'_338 ::
  Integer -> Integer -> Integer -> Integer -> Integer -> Integer
d_mod'8322'_338 :: Integer -> Integer -> Integer -> Integer -> Integer -> Integer
d_mod'8322'_338 Integer
v0 Integer
v1 ~Integer
v2 = Integer -> Integer -> Integer -> Integer -> Integer
du_mod'8322'_338 Integer
v0 Integer
v1
du_mod'8322'_338 ::
  Integer -> Integer -> Integer -> Integer -> Integer
du_mod'8322'_338 :: Integer -> Integer -> Integer -> Integer -> Integer
du_mod'8322'_338 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Integer
forall a b. a -> b
coe
      Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90
      (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
      (Integer -> Integer -> Integer
addInt ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
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
v0)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
-- Data.Nat.DivMod.Core.div-cong₃
d_div'45'cong'8323'_358 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'45'cong'8323'_358 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8801'__12
-> T__'8801'__12
d_div'45'cong'8323'_358 = Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.acc≤divₕ[acc]
d_acc'8804'div'8341''91'acc'93'_368 ::
  Integer ->
  Integer ->
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_acc'8804'div'8341''91'acc'93'_368 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__22
d_acc'8804'div'8341''91'acc'93'_368 Integer
v0 Integer
v1 Integer
v2 Integer
v3
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
      Integer
0 -> (Integer -> T__'8804'__22) -> Any -> T__'8804'__22
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)
      Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T__'8804'__22
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v3 of
                Integer
0 -> (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'trans_2784
                       ((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
                          Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_2844 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                       ((Integer -> Integer -> Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer -> Integer -> T__'8804'__22
d_acc'8804'div'8341''91'acc'93'_368
                          ((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
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v4)
                          (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                Integer
_ -> let v5 :: Integer
v5 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
forall a b. a -> b
coe
                       ((Integer -> Integer -> Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer -> Integer -> T__'8804'__22
d_acc'8804'div'8341''91'acc'93'_368 (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
v4)
                          (Integer -> Any
forall a b. a -> b
coe Integer
v5)))
-- Data.Nat.DivMod.Core.divₕ-offsetEq
d_div'8341''45'offsetEq_410 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'8341''45'offsetEq_410 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8846'__30
-> T__'8801'__12
d_div'8341''45'offsetEq_410 = Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8846'__30
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.div-mod-lemma
d_div'45'mod'45'lemma_656 ::
  Integer ->
  Integer ->
  Integer ->
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'45'mod'45'lemma_656 :: Integer -> Integer -> Integer -> Integer -> T__'8801'__12
d_div'45'mod'45'lemma_656 = Integer -> Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core._.m
d_m_686 :: Integer -> Integer -> Integer -> Integer -> Integer
d_m_686 :: Integer -> Integer -> Integer -> Integer -> Integer
d_m_686 Integer
v0 Integer
v1 ~Integer
v2 ~Integer
v3 = Integer -> Integer -> Integer
du_m_686 Integer
v0 Integer
v1
du_m_686 :: Integer -> Integer -> Integer
du_m_686 :: Integer -> Integer -> Integer
du_m_686 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
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
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Nat.DivMod.Core.divₕ-restart
d_div'8341''45'restart_700 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'8341''45'restart_700 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8801'__12
d_div'8341''45'restart_700 = Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.divₕ-extractAcc
d_div'8341''45'extractAcc_724 ::
  Integer ->
  Integer ->
  Integer ->
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'8341''45'extractAcc_724 :: Integer -> Integer -> Integer -> Integer -> T__'8801'__12
d_div'8341''45'extractAcc_724 = Integer -> Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.divₕ-finish
d_div'8341''45'finish_756 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'8341''45'finish_756 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8801'__12
d_div'8341''45'finish_756 = Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.n[divₕ]n≡1
d_n'91'div'8341''93'n'8801'1_776 ::
  Integer ->
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_n'91'div'8341''93'n'8801'1_776 :: Integer -> Integer -> T__'8801'__12
d_n'91'div'8341''93'n'8801'1_776 = Integer -> Integer -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.a[divₕ]1≡a
d_a'91'div'8341''93'1'8801'a_788 ::
  Integer ->
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_a'91'div'8341''93'1'8801'a_788 :: Integer -> Integer -> T__'8801'__12
d_a'91'div'8341''93'1'8801'a_788 = Integer -> Integer -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.a*n[divₕ]n≡a
d_a'42'n'91'div'8341''93'n'8801'a_802 ::
  Integer ->
  Integer ->
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_a'42'n'91'div'8341''93'n'8801'a_802 :: Integer -> Integer -> Integer -> T__'8801'__12
d_a'42'n'91'div'8341''93'n'8801'a_802 = Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.+-distrib-divₕ
d_'43''45'distrib'45'div'8341'_824 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'43''45'distrib'45'div'8341'_824 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8801'__12
d_'43''45'distrib'45'div'8341'_824 = Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core._.case
d_case_870 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_case_870 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8846'__30
d_case_870 ~Integer
v0 Integer
v1 ~Integer
v2 Integer
v3 T__'8804'__22
v4 = Integer -> Integer -> T__'8804'__22 -> T__'8846'__30
du_case_870 Integer
v1 Integer
v3 T__'8804'__22
v4
du_case_870 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_case_870 :: Integer -> Integer -> T__'8804'__22 -> T__'8846'__30
du_case_870 Integer
v0 Integer
v1 T__'8804'__22
v2
  = (Any -> T__'8846'__30) -> Any -> T__'8846'__30
forall a b. a -> b
coe
      Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
      ((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 -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
            Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased
            ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
               Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
               ((Integer -> T__'8804'__22 -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
                  Integer -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'43''45'cancel'737''45''8804'_3414
                  ((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
v0)) (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v2))
               ((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
                  Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'n'43'm_3494 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))))
-- Data.Nat.DivMod.Core.divₕ-mono-≤
d_div'8341''45'mono'45''8804'_886 ::
  Integer ->
  Integer ->
  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
d_div'8341''45'mono'45''8804'_886 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
d_div'8341''45'mono'45''8804'_886 Integer
v0 Integer
v1 Integer
v2 Integer
v3 Integer
v4 Integer
v5 T__'8804'__22
v6 T__'8804'__22
v7
  = case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v6 of
      T__'8804'__22
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_26
        -> (Integer -> Integer -> Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
             Integer -> Integer -> Integer -> Integer -> T__'8804'__22
d_acc'8804'div'8341''91'acc'93'_368
             ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60 Integer
v0
                (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) (Integer
0 :: Integer) Integer
v4)
             ((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
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v5)) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v5)
      MAlonzo.Code.Data.Nat.Base.C_s'8804's_34 T__'8804'__22
v10
        -> let v11 :: Integer
v11 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T__'8804'__22
forall a b. a -> b
coe
             (let v12 :: Integer
v12 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
              Any -> Any
forall a b. a -> b
coe
                (let v13 :: b
v13
                       = Any -> b -> b
forall a b. a -> b -> b
seq
                           (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v7)
                           (let v13 :: t
v13
                                  = ((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
v13 ->
                                         (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 -> 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
v4)))
                                      ((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_Dec_20) -> Any -> Any
forall a b. a -> b
coe
                                         Bool -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_T'63'_66
                                         ((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
                                            Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__14
                                            ((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
v4)) (Integer -> Any
forall a b. a -> b
coe Integer
v2))) in
                            Any -> b
forall a b. a -> b
coe
                              (case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v13 of
                                 MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v14 T_Reflects_16
v15
                                   -> if Bool -> Bool
forall a b. a -> b
coe Bool
v14
                                        then (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
v15)
                                               (((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
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
v16 Any
v17 Any
v18 ->
                                                        (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
v18))
                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                     Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2 Integer
v4)
                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                     (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1 Integer
v12
                                                     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
-> 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
v16 Any
v17 Any
v18 Any
v19 Any
v20 -> Any
v20)
                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                        Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2 Integer
v4)
                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                        ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                           Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                           Integer
v11 Integer
v4)
                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)))
                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
                                                        Integer
v12 Integer
v1)
                                                     (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> T__'8804'__22 -> 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
v16 Any
v17 Any
v18 Any
v19 Any
v20 ->
                                                              (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
v19 Any
v20))
                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                           (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                           (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                           ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                              Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                              Integer
v11 Integer
v4)
                                                           (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)))
                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                           (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
                                                           Integer
v12 Integer
v1)
                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                           (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
                                                           Integer
v12 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 -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                              (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                              Integer
v1 Integer
v12 Integer
v1))
                                                        (Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
d_div'8341''45'mono'45''8804'_886
                                                           ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
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
v0))
                                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                           ((Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b
coe
                                                              Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                              Integer
v11 Integer
v4)
                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v12) ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v1)
                                                           ((T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
                                                              T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_2784
                                                              ((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                 Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_5042
                                                                 (Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                                                              (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v10))
                                                           ((Integer -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
                                                              Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_3482
                                                              (Integer -> Any
forall a b. a -> b
coe Integer
v1))))
                                                     Any
forall a. a
erased))
                                        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
v15)
                                               (((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
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
v16 Any
v17 Any
v18 ->
                                                        (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
v18))
                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                     Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2 Integer
v4)
                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                     (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1 Integer
v12
                                                     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
-> 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
v16 Any
v17 Any
v18 Any
v19 Any
v20 -> Any
v20)
                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                        Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2 Integer
v4)
                                                     Integer
v0
                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
                                                        Integer
v12 Integer
v1)
                                                     (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> Any -> T__'8804'__22 -> 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
v16 Any
v17 Any
v18 Any
v19 Any
v20 ->
                                                              (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
v19 Any
v20))
                                                        Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                           (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
                                                           Integer
v12 Integer
v1)
                                                        (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Any -> Any -> Any -> T__'8804'__22 -> 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
v16 Any
v17 Any
v18 Any
v19 Any
v20 ->
                                                                 (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
v19 Any
v20))
                                                           (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                           ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                              (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                              Integer
v1 Integer
v12 Integer
v1)
                                                           ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                              (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                              Integer
v1 Integer
v12 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 -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                 Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                 (Integer -> Integer -> Integer
addInt
                                                                    (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                 Integer
v1 Integer
v12 Integer
v1))
                                                           (Integer -> Integer -> Integer -> Integer -> T__'8804'__22
d_acc'8804'div'8341''91'acc'93'_368
                                                              ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
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
v0))
                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v12) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)))
                                                        (Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_2844
                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0)))
                                                     Any
forall a. a
erased))
                                 T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
                 Any -> Any
forall a b. a -> b
coe
                   (case Integer -> Integer
forall a b. a -> b
coe Integer
v4 of
                      Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v5 of
                             Integer
0 -> case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v7 of
                                    T__'8804'__22
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_26
                                      -> let v15 :: Integer
v15 = Integer
0 :: Integer in
                                         Any -> Any
forall a b. a -> b
coe
                                           (let v16 :: t
v16
                                                  = ((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
v16 ->
                                                         (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
1 :: Integer)))
                                                      ((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_Dec_20) -> Any -> Any
forall a b. a -> b
coe
                                                         Bool -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_T'63'_66
                                                         ((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                            Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__14
                                                            (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v2))) in
                                            Any -> Any
forall a b. a -> b
coe
                                              (case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v16 of
                                                 MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v17 T_Reflects_16
v18
                                                   -> if Bool -> Bool
forall a b. a -> b
coe Bool
v17
                                                        then (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
v18)
                                                               (((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
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
v19 Any
v20 Any
v21 ->
                                                                        (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
v21))
                                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                     Integer
v0 Integer
v1 Integer
v2 Integer
v15)
                                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                     (Integer -> Integer -> Integer
addInt
                                                                        (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                        (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                     Integer
v1 Integer
v12 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
-> 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
v19 Any
v20 Any
v21 Any
v22 Any
v23 -> Any
v23)
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        Integer
v0 Integer
v1 Integer
v2 Integer
v15)
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        (Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                        Integer
v1
                                                                        ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                           Integer
v11 Integer
v15)
                                                                        Integer
v1)
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        (Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                        Integer
v1 Integer
v12 Integer
v1)
                                                                     (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> T__'8804'__22 -> 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
v19 Any
v20 Any
v21 Any
v22 Any
v23 ->
                                                                              (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
v22 Any
v23))
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           Integer
v1
                                                                           ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                              Integer
v11 Integer
v15)
                                                                           Integer
v1)
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           Integer
v1 Integer
v12 Integer
v1)
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           Integer
v1 Integer
v12 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 -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                              (Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Integer
forall a b. a -> b
coe
                                                                                    (Integer
1 :: Integer))
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                              Integer
v1 Integer
v12 Integer
v1))
                                                                        (Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
d_div'8341''45'mono'45''8804'_886
                                                                           ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
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
v0))
                                                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                                           ((Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                              Integer
v11 Integer
v15)
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v12) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v1)
                                                                           ((T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
                                                                              T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_2784
                                                                              ((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                 Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_5042
                                                                                 (Integer -> Any
forall a b. a -> b
coe Integer
v11)
                                                                                 (Integer -> Any
forall a b. a -> b
coe Integer
v15))
                                                                              (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v10))
                                                                           ((Integer -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
                                                                              Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_3482
                                                                              (Integer -> Any
forall a b. a -> b
coe Integer
v1))))
                                                                     Any
forall a. a
erased))
                                                        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
v18)
                                                               (((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
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
v19 Any
v20 Any
v21 ->
                                                                        (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
v21))
                                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                     Integer
v0 Integer
v1 Integer
v2 Integer
v15)
                                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                     (Integer -> Integer -> Integer
addInt
                                                                        (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                        (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                     Integer
v1 Integer
v12 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
-> 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
v19 Any
v20 Any
v21 Any
v22 Any
v23 -> Any
v23)
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        Integer
v0 Integer
v1 Integer
v2 Integer
v15)
                                                                     Integer
v0
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        (Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                        Integer
v1 Integer
v12 Integer
v1)
                                                                     (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> Any -> T__'8804'__22 -> 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
v19 Any
v20 Any
v21 Any
v22 Any
v23 ->
                                                                              (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
v22 Any
v23))
                                                                        Integer
v0
                                                                        (Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           Integer
v1 Integer
v12 Integer
v1)
                                                                        (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Any -> Any -> Any -> T__'8804'__22 -> 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
v19 Any
v20 Any
v21 Any
v22
                                                                                 Any
v23 ->
                                                                                 (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
v22 Any
v23))
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                              (Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Integer
forall a b. a -> b
coe
                                                                                    (Integer
1 :: Integer))
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                              Integer
v1 Integer
v12 Integer
v1)
                                                                           ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                              (Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Integer
forall a b. a -> b
coe
                                                                                    (Integer
1 :: Integer))
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                              Integer
v1 Integer
v12 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 -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                                 Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                                 (Integer -> Integer -> Integer
addInt
                                                                                    (Integer -> Integer
forall a b. a -> b
coe
                                                                                       (Integer
1 ::
                                                                                          Integer))
                                                                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                                 Integer
v1 Integer
v12 Integer
v1))
                                                                           (Integer -> Integer -> Integer -> Integer -> T__'8804'__22
d_acc'8804'div'8341''91'acc'93'_368
                                                                              ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
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
v0))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v12)
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v1)))
                                                                        (Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_2844
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0)))
                                                                     Any
forall a. a
erased))
                                                 T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
                                    T__'8804'__22
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                             Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v13
                      Integer
_ -> let v14 :: Integer
v14 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v4) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                           Any -> Any
forall a b. a -> b
coe
                             (case Integer -> Integer
forall a b. a -> b
coe Integer
v5 of
                                Integer
0 -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                       Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v7)
                                       (let v15 :: t
v15
                                              = ((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
v15 ->
                                                     (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 -> 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
v4)))
                                                  ((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_Dec_20) -> Any -> Any
forall a b. a -> b
coe
                                                     Bool -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_T'63'_66
                                                     ((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                        Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__14
                                                        ((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
v4))
                                                        (Integer -> Any
forall a b. a -> b
coe Integer
v2))) in
                                        Any -> Any
forall a b. a -> b
coe
                                          (case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v15 of
                                             MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v16 T_Reflects_16
v17
                                               -> if Bool -> Bool
forall a b. a -> b
coe Bool
v16
                                                    then (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
v17)
                                                           (((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
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
v18 Any
v19 Any
v20 ->
                                                                    (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
v20))
                                                              ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                 Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                 Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2
                                                                 Integer
v4)
                                                              ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                 Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                 (Integer -> Integer -> Integer
addInt
                                                                    (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                 Integer
v1 Integer
v12 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
-> 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
v18 Any
v19 Any
v20 Any
v21 Any
v22 -> Any
v22)
                                                                 ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                    Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                    Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2
                                                                    Integer
v4)
                                                                 ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
                                                                    Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                    (Integer -> Integer -> Integer
addInt
                                                                       (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                    (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                                    ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                       Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                       Integer
v11 Integer
v4)
                                                                    (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)))
                                                                 ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                    Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                    (Integer -> Integer -> Integer
addInt
                                                                       (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                    Integer
v1 Integer
v12 Integer
v1)
                                                                 (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> T__'8804'__22 -> 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
v18 Any
v19 Any
v20 Any
v21 Any
v22 ->
                                                                          (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
v21 Any
v22))
                                                                    ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
                                                                       Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                       (Integer -> Integer -> Integer
addInt
                                                                          (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                          (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                       (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                                       ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                          Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                          Integer
v11 Integer
v4)
                                                                       (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)))
                                                                    ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                       Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                       (Integer -> Integer -> Integer
addInt
                                                                          (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                          (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                       Integer
v1 Integer
v12 Integer
v1)
                                                                    ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                       Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                       (Integer -> Integer -> Integer
addInt
                                                                          (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                          (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                       Integer
v1 Integer
v12 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 -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                          Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                          (Integer -> Integer -> Integer
addInt
                                                                             (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                             (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                          Integer
v1 Integer
v12 Integer
v1))
                                                                    (Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
d_div'8341''45'mono'45''8804'_886
                                                                       ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
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
v0))
                                                                       (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                                       ((Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b
coe
                                                                          Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                          Integer
v11 Integer
v4)
                                                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v12)
                                                                       ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
                                                                          Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                                                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v1)
                                                                       ((T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
                                                                          T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_2784
                                                                          ((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                             Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_5042
                                                                             (Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                                                                          (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v10))
                                                                       ((Integer -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
                                                                          Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_3482
                                                                          (Integer -> Any
forall a b. a -> b
coe Integer
v1))))
                                                                 Any
forall a. a
erased))
                                                    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
v17)
                                                           (((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
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
v18 Any
v19 Any
v20 ->
                                                                    (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
v20))
                                                              ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                 Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                 Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2
                                                                 Integer
v4)
                                                              ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                 Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                 (Integer -> Integer -> Integer
addInt
                                                                    (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                 Integer
v1 Integer
v12 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
-> 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
v18 Any
v19 Any
v20 Any
v21 Any
v22 -> Any
v22)
                                                                 ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                    Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                    Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2
                                                                    Integer
v4)
                                                                 Integer
v0
                                                                 ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                    Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                    (Integer -> Integer -> Integer
addInt
                                                                       (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                    Integer
v1 Integer
v12 Integer
v1)
                                                                 (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> Any -> T__'8804'__22 -> 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
v18 Any
v19 Any
v20 Any
v21 Any
v22 ->
                                                                          (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
v21 Any
v22))
                                                                    Integer
v0
                                                                    (Integer -> Integer -> Integer
addInt
                                                                       (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                    ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                       Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                       (Integer -> Integer -> Integer
addInt
                                                                          (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                          (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                       Integer
v1 Integer
v12 Integer
v1)
                                                                    (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Any -> Any -> Any -> T__'8804'__22 -> 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
v18 Any
v19 Any
v20 Any
v21 Any
v22 ->
                                                                             (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
v21 Any
v22))
                                                                       (Integer -> Integer -> Integer
addInt
                                                                          (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                          (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                       ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                          Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                          (Integer -> Integer -> Integer
addInt
                                                                             (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                             (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                          Integer
v1 Integer
v12 Integer
v1)
                                                                       ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                          Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                          (Integer -> Integer -> Integer
addInt
                                                                             (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                             (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                          Integer
v1 Integer
v12 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 -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                             Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                             (Integer -> Integer -> Integer
addInt
                                                                                (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                                (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                             Integer
v1 Integer
v12 Integer
v1))
                                                                       (Integer -> Integer -> Integer -> Integer -> T__'8804'__22
d_acc'8804'div'8341''91'acc'93'_368
                                                                          ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
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
v0))
                                                                          (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v12)
                                                                          (Integer -> Integer
forall a b. a -> b
coe Integer
v1)))
                                                                    (Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_2844
                                                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v0)))
                                                                 Any
forall a. a
erased))
                                             T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
                                Integer
_ -> let v15 :: Integer
v15 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v5) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                                     Any -> Any
forall a b. a -> b
coe
                                       (case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v7 of
                                          MAlonzo.Code.Data.Nat.Base.C_s'8804's_34 T__'8804'__22
v18
                                            -> (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
d_div'8341''45'mono'45''8804'_886 (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
v1))
                                                 (Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v12) (Integer -> Any
forall a b. a -> b
coe Integer
v14) (Integer -> Any
forall a b. a -> b
coe Integer
v15) (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v10)
                                                 (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v18)
                                          T__'8804'__22
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_26
                                            -> let v17 :: t
v17
                                                     = ((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
v17 ->
                                                            (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 -> 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
v4)))
                                                         ((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_Dec_20) -> Any -> Any
forall a b. a -> b
coe
                                                            Bool -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_T'63'_66
                                                            ((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                               Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__14
                                                               ((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
v4))
                                                               (Integer -> Any
forall a b. a -> b
coe Integer
v2))) in
                                               Any -> Any
forall a b. a -> b
coe
                                                 (case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v17 of
                                                    MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v18 T_Reflects_16
v19
                                                      -> if Bool -> Bool
forall a b. a -> b
coe Bool
v18
                                                           then (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
v19)
                                                                  (((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
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
v20 Any
v21 Any
v22 ->
                                                                           (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
v22))
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        Integer
v0
                                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                                        Integer
v2 Integer
v4)
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        (Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                        Integer
v1 Integer
v12 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
-> 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
v20 Any
v21 Any
v22 Any
v23 Any
v24 ->
                                                                           Any
v24)
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           Integer
v0
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                                           Integer
v2 Integer
v4)
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                                           ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                              Integer
v11 Integer
v4)
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)))
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           Integer
v1 Integer
v12 Integer
v1)
                                                                        (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> T__'8804'__22 -> 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
v20 Any
v21 Any
v22 Any
v23
                                                                                 Any
v24 ->
                                                                                 (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
v23 Any
v24))
                                                                           ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                              (Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Integer
forall a b. a -> b
coe
                                                                                    (Integer
1 :: Integer))
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                              (Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                                              ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                                 Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                                 Integer
v11 Integer
v4)
                                                                              (Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)))
                                                                           ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                              (Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Integer
forall a b. a -> b
coe
                                                                                    (Integer
1 :: Integer))
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                              Integer
v1 Integer
v12 Integer
v1)
                                                                           ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                              (Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Integer
forall a b. a -> b
coe
                                                                                    (Integer
1 :: Integer))
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                              Integer
v1 Integer
v12 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 -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                                 Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                                 (Integer -> Integer -> Integer
addInt
                                                                                    (Integer -> Integer
forall a b. a -> b
coe
                                                                                       (Integer
1 ::
                                                                                          Integer))
                                                                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                                 Integer
v1 Integer
v12 Integer
v1))
                                                                           (Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
d_div'8341''45'mono'45''8804'_886
                                                                              ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
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
v0))
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                                              ((Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b
coe
                                                                                 Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                                 Integer
v11 Integer
v4)
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v12)
                                                                              ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
                                                                                 Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v1)
                                                                                 (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v1)
                                                                              ((T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
                                                                                 T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_2784
                                                                                 ((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                    Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_5042
                                                                                    (Integer -> Any
forall a b. a -> b
coe Integer
v11)
                                                                                    (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                                                                                 (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v10))
                                                                              ((Integer -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
                                                                                 Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_3482
                                                                                 (Integer -> Any
forall a b. a -> b
coe Integer
v1))))
                                                                        Any
forall a. a
erased))
                                                           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
v19)
                                                                  (((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
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
v20 Any
v21 Any
v22 ->
                                                                           (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
v22))
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        Integer
v0
                                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                                        Integer
v2 Integer
v4)
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        (Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                        Integer
v1 Integer
v12 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
-> 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
v20 Any
v21 Any
v22 Any
v23 Any
v24 ->
                                                                           Any
v24)
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           Integer
v0
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                                           Integer
v2 Integer
v4)
                                                                        Integer
v0
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           Integer
v1 Integer
v12 Integer
v1)
                                                                        (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> Any -> T__'8804'__22 -> 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
v20 Any
v21 Any
v22 Any
v23
                                                                                 Any
v24 ->
                                                                                 (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
v23 Any
v24))
                                                                           Integer
v0
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                              (Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Integer
forall a b. a -> b
coe
                                                                                    (Integer
1 :: Integer))
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                              Integer
v1 Integer
v12 Integer
v1)
                                                                           (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Any -> Any -> Any -> T__'8804'__22 -> 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
v20 Any
v21 Any
v22 Any
v23
                                                                                    Any
v24 ->
                                                                                    (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
v23 Any
v24))
                                                                              (Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Integer
forall a b. a -> b
coe
                                                                                    (Integer
1 :: Integer))
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                              ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                                 Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                                 (Integer -> Integer -> Integer
addInt
                                                                                    (Integer -> Integer
forall a b. a -> b
coe
                                                                                       (Integer
1 ::
                                                                                          Integer))
                                                                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                                 Integer
v1 Integer
v12 Integer
v1)
                                                                              ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                                 Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                                 (Integer -> Integer -> Integer
addInt
                                                                                    (Integer -> Integer
forall a b. a -> b
coe
                                                                                       (Integer
1 ::
                                                                                          Integer))
                                                                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                                 Integer
v1 Integer
v12 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 -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                                    Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                                    (Integer -> Integer -> Integer
addInt
                                                                                       (Integer -> Integer
forall a b. a -> b
coe
                                                                                          (Integer
1 ::
                                                                                             Integer))
                                                                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                                    Integer
v1 Integer
v12 Integer
v1))
                                                                              (Integer -> Integer -> Integer -> Integer -> T__'8804'__22
d_acc'8804'div'8341''91'acc'93'_368
                                                                                 ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
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
v0))
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v12)
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v1)))
                                                                           (Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_2844
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0)))
                                                                        Any
forall a. a
erased))
                                                    T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                                          T__'8804'__22
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))))
      T__'8804'__22
_ -> T__'8804'__22
forall a. a
MAlonzo.RTE.mazUnreachableError