{-# 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.Divisibility 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Nat
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Nat.Divisibility.Core
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Core
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Base.Double
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Syntax
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Data.Nat.Divisibility.quotient≢0
d_quotient'8802'0_18 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112
d_quotient'8802'0_18 :: Integer
-> Integer -> T__'8739'__20 -> T_NonZero_112 -> T_NonZero_112
d_quotient'8802'0_18 ~Integer
v0 ~Integer
v1 ~T__'8739'__20
v2 ~T_NonZero_112
v3 = T_NonZero_112
du_quotient'8802'0_18
du_quotient'8802'0_18 :: MAlonzo.Code.Data.Nat.Base.T_NonZero_112
du_quotient'8802'0_18 :: T_NonZero_112
du_quotient'8802'0_18
  = T_NonZero_112 -> T_NonZero_112
forall a b. a -> b
coe
      T_NonZero_112
MAlonzo.Code.Data.Nat.Properties.du_m'42'n'8802'0'8658'm'8802'0_3850
-- Data.Nat.Divisibility.m∣n⇒n≡quotient*m
d_m'8739'n'8658'n'8801'quotient'42'm_28 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'8739'n'8658'n'8801'quotient'42'm_28 :: Integer -> Integer -> T__'8739'__20 -> T__'8801'__12
d_m'8739'n'8658'n'8801'quotient'42'm_28 = Integer -> Integer -> T__'8739'__20 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.Divisibility.m∣n⇒n≡m*quotient
d_m'8739'n'8658'n'8801'm'42'quotient_34 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'8739'n'8658'n'8801'm'42'quotient_34 :: Integer -> Integer -> T__'8739'__20 -> T__'8801'__12
d_m'8739'n'8658'n'8801'm'42'quotient_34 = Integer -> Integer -> T__'8739'__20 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.Divisibility.quotient-∣
d_quotient'45''8739'_46 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_quotient'45''8739'_46 :: Integer -> Integer -> T__'8739'__20 -> T__'8739'__20
d_quotient'45''8739'_46 Integer
v0 ~Integer
v1 ~T__'8739'__20
v2 = Integer -> T__'8739'__20
du_quotient'45''8739'_46 Integer
v0
du_quotient'45''8739'_46 ::
  Integer -> MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_quotient'45''8739'_46 :: Integer -> T__'8739'__20
du_quotient'45''8739'_46 Integer
v0
  = (Integer -> T__'8739'__20) -> Integer -> T__'8739'__20
forall a b. a -> b
coe Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v0
-- Data.Nat.Divisibility.quotient>1
d_quotient'62'1_54 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_quotient'62'1_54 :: Integer
-> Integer -> T__'8739'__20 -> T__'8804'__22 -> T__'8804'__22
d_quotient'62'1_54 Integer
v0 Integer
v1 T__'8739'__20
v2 T__'8804'__22
v3
  = (Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22)
-> Integer -> Integer -> Integer -> Any -> T__'8804'__22
forall a b. a -> b
coe
      Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_'42''45'cancel'737''45''60'_4208
      Integer
v0 (Integer
1 :: Integer)
      (T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v2))
      (let v4 :: b
v4
             = T_SubRelation_60 -> b
forall a b. a -> b
coe
                 T_SubRelation_60
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_strictRelation_202 in
       Any -> Any
forall a b. a -> b
coe
         ((T_SubRelation_60 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
            T_SubRelation_60 -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__126
            (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)))
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v0)
               ((T__'8739'__20 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                  T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v2)))
            (((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
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))) Integer
v0
               (Integer -> Integer -> Integer
mulInt
                  (Integer -> Integer
forall a b. a -> b
coe Integer
v0)
                  ((T__'8739'__20 -> Integer) -> Any -> Integer
forall a b. a -> b
coe
                     T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v2)))
               (((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''60'_312
                  (((Any -> Any -> Any -> Any -> Any -> Any)
 -> T_Σ_14
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
forall a b. a -> b
coe
                     (Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'60''45'go_152
                     (\ Any
v5 Any
v6 Any
v7 Any
v8 Any
v9 ->
                        (Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans_2980 Any
v6 Any
v8 Any
v9)
                     (T_Σ_14 -> Any
forall a b. a -> b
coe
                        T_Σ_14
MAlonzo.Code.Relation.Binary.PropositionalEquality.Core.du_resp'8322'_160)
                     (\ Any
v5 Any
v6 Any
v7 Any
v8 Any
v9 ->
                        (T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
                          T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45''8804''45'trans_2992 Any
v8
                          Any
v9))
                  Integer
v0 Integer
v1
                  (Integer -> Integer -> Integer
mulInt
                     (Integer -> Integer
forall a b. a -> b
coe Integer
v0)
                     ((T__'8739'__20 -> Integer) -> Any -> Integer
forall a b. a -> b
coe
                        T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v2)))
                  (((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
v1
                     (Integer -> Integer -> Integer
mulInt
                        (Integer -> Integer
forall a b. a -> b
coe Integer
v0)
                        ((T__'8739'__20 -> Integer) -> Any -> Integer
forall a b. a -> b
coe
                           T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v2)))
                     (Integer -> Integer -> Integer
mulInt
                        (Integer -> Integer
forall a b. a -> b
coe Integer
v0)
                        ((T__'8739'__20 -> Integer) -> Any -> Integer
forall a b. a -> b
coe
                           T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v2)))
                     (((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                        (Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
                        ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
                           T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
                           (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
                        ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                           Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v0)
                           ((T__'8739'__20 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                              T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v2))))
                     Any
forall a. a
erased)
                  T__'8804'__22
v3)
               Any
forall a. a
erased)))
-- Data.Nat.Divisibility.quotient-<
d_quotient'45''60'_70 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Base.T_NonTrivial_152 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_quotient'45''60'_70 :: Integer
-> Integer
-> T__'8739'__20
-> T_NonTrivial_152
-> T_NonZero_112
-> T__'8804'__22
d_quotient'45''60'_70 Integer
v0 Integer
v1 T__'8739'__20
v2 ~T_NonTrivial_152
v3 ~T_NonZero_112
v4
  = Integer -> Integer -> T__'8739'__20 -> T__'8804'__22
du_quotient'45''60'_70 Integer
v0 Integer
v1 T__'8739'__20
v2
du_quotient'45''60'_70 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_quotient'45''60'_70 :: Integer -> Integer -> T__'8739'__20 -> T__'8804'__22
du_quotient'45''60'_70 Integer
v0 Integer
v1 T__'8739'__20
v2
  = let v3 :: b
v3
          = T_SubRelation_60 -> b
forall a b. a -> b
coe
              T_SubRelation_60
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_strictRelation_202 in
    Any -> T__'8804'__22
forall a b. a -> b
coe
      ((T_SubRelation_60 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
         T_SubRelation_60 -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__126
         (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v3)
         ((T__'8739'__20 -> Integer) -> Any -> Any
forall a b. a -> b
coe
            T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v2))
         (Integer -> Any
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''60'_312
            (((Any -> Any -> Any -> Any -> Any -> Any)
 -> T_Σ_14
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
forall a b. a -> b
coe
               (Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'60''45'go_152
               (\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
                  (Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                    Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans_2980 Any
v5 Any
v7 Any
v8)
               (T_Σ_14 -> Any
forall a b. a -> b
coe
                  T_Σ_14
MAlonzo.Code.Relation.Binary.PropositionalEquality.Core.du_resp'8322'_160)
               (\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
                  (T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
                    T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45''8804''45'trans_2992 Any
v7
                    Any
v8))
            (T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v2))
            (Integer -> Integer -> Integer
mulInt
               ((T__'8739'__20 -> Integer) -> Any -> Integer
forall a b. a -> b
coe
                  T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v2))
               (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
            Integer
v1
            (((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
               (Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
               (\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 -> Any
v8)
               (Integer -> Integer -> Integer
mulInt
                  ((T__'8739'__20 -> Integer) -> Any -> Integer
forall a b. a -> b
coe
                     T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v2))
                  (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
               Integer
v1 Integer
v1
               (((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                  (Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
                  ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
                     T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
                     (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
                  (Integer -> Any
forall a b. a -> b
coe Integer
v1))
               Any
forall a. a
erased)
            ((Integer -> Integer -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'60'm'42'n_4152
               ((T__'8739'__20 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                  T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v2))
               (Integer -> Any
forall a b. a -> b
coe Integer
v0)
               (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
MAlonzo.Code.Data.Nat.Base.du_nonTrivial'8658'n'62'1_174))))
-- Data.Nat.Divisibility.n/m≡quotient
d_n'47'm'8801'quotient_88 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_n'47'm'8801'quotient_88 :: Integer
-> Integer -> T__'8739'__20 -> T_NonZero_112 -> T__'8801'__12
d_n'47'm'8801'quotient_88 = Integer
-> Integer -> T__'8739'__20 -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.Divisibility.m%n≡0⇒n∣m
d_m'37'n'8801'0'8658'n'8739'm_100 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_m'37'n'8801'0'8658'n'8739'm_100 :: Integer
-> Integer -> T_NonZero_112 -> T__'8801'__12 -> T__'8739'__20
d_m'37'n'8801'0'8658'n'8739'm_100 Integer
v0 Integer
v1 ~T_NonZero_112
v2 ~T__'8801'__12
v3
  = Integer -> Integer -> T__'8739'__20
du_m'37'n'8801'0'8658'n'8739'm_100 Integer
v0 Integer
v1
du_m'37'n'8801'0'8658'n'8739'm_100 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_m'37'n'8801'0'8658'n'8739'm_100 :: Integer -> Integer -> T__'8739'__20
du_m'37'n'8801'0'8658'n'8739'm_100 Integer
v0 Integer
v1
  = (Integer -> T__'8739'__20) -> Any -> T__'8739'__20
forall a b. a -> b
coe
      Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34
      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
-- Data.Nat.Divisibility._.[m/n]*n
d_'91'm'47'n'93''42'n_112 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> Integer
d_'91'm'47'n'93''42'n_112 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12 -> Integer
d_'91'm'47'n'93''42'n_112 Integer
v0 Integer
v1 ~T_NonZero_112
v2 ~T__'8801'__12
v3
  = Integer -> Integer -> Integer
du_'91'm'47'n'93''42'n_112 Integer
v0 Integer
v1
du_'91'm'47'n'93''42'n_112 :: Integer -> Integer -> Integer
du_'91'm'47'n'93''42'n_112 :: Integer -> Integer -> Integer
du_'91'm'47'n'93''42'n_112 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
      Integer -> Integer -> Integer
mulInt
      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
      (Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Nat.Divisibility.n∣m⇒m%n≡0
d_n'8739'm'8658'm'37'n'8801'0_122 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_n'8739'm'8658'm'37'n'8801'0_122 :: Integer
-> Integer -> T_NonZero_112 -> T__'8739'__20 -> T__'8801'__12
d_n'8739'm'8658'm'37'n'8801'0_122 = Integer
-> Integer -> T_NonZero_112 -> T__'8739'__20 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.Divisibility.m%n≡0⇔n∣m
d_m'37'n'8801'0'8660'n'8739'm_134 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_m'37'n'8801'0'8660'n'8739'm_134 :: Integer -> Integer -> T_NonZero_112 -> T_Equivalence_1714
d_m'37'n'8801'0'8660'n'8739'm_134 Integer
v0 Integer
v1 ~T_NonZero_112
v2
  = Integer -> Integer -> T_Equivalence_1714
du_m'37'n'8801'0'8660'n'8739'm_134 Integer
v0 Integer
v1
du_m'37'n'8801'0'8660'n'8739'm_134 ::
  Integer ->
  Integer -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_m'37'n'8801'0'8660'n'8739'm_134 :: Integer -> Integer -> T_Equivalence_1714
du_m'37'n'8801'0'8660'n'8739'm_134 Integer
v0 Integer
v1
  = ((Any -> Any) -> (Any -> Any) -> T_Equivalence_1714)
-> (Any -> Any) -> Any -> T_Equivalence_1714
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
      (\ Any
v2 -> (Integer -> Integer -> T__'8739'__20) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T__'8739'__20
du_m'37'n'8801'0'8658'n'8739'm_100 (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
-- Data.Nat.Divisibility.∣⇒≤
d_'8739''8658''8804'_142 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_'8739''8658''8804'_142 :: Integer
-> Integer -> T_NonZero_112 -> T__'8739'__20 -> T__'8804'__22
d_'8739''8658''8804'_142 ~Integer
v0 Integer
v1 ~T_NonZero_112
v2 T__'8739'__20
v3
  = Integer -> T__'8739'__20 -> T__'8804'__22
du_'8739''8658''8804'_142 Integer
v1 T__'8739'__20
v3
du_'8739''8658''8804'_142 ::
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_'8739''8658''8804'_142 :: Integer -> T__'8739'__20 -> T__'8804'__22
du_'8739''8658''8804'_142 Integer
v0 T__'8739'__20
v1
  = (Any -> Any -> Any) -> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
      Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
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'm'43'n_3482 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
-- Data.Nat.Divisibility.>⇒∤
d_'62''8658''8740'_154 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'62''8658''8740'_154 :: Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8739'__20
-> T_Irrelevant_20
d_'62''8658''8740'_154 = Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8739'__20
-> T_Irrelevant_20
forall a. a
erased
-- Data.Nat.Divisibility.∣-reflexive
d_'8739''45'reflexive_162 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'8739''45'reflexive_162 :: Integer -> Integer -> T__'8801'__12 -> T__'8739'__20
d_'8739''45'reflexive_162 ~Integer
v0 ~Integer
v1 ~T__'8801'__12
v2 = T__'8739'__20
du_'8739''45'reflexive_162
du_'8739''45'reflexive_162 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'8739''45'reflexive_162 :: T__'8739'__20
du_'8739''45'reflexive_162
  = (Integer -> T__'8739'__20) -> Integer -> T__'8739'__20
forall a b. a -> b
coe
      Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 (Integer
1 :: Integer)
-- Data.Nat.Divisibility.∣-refl
d_'8739''45'refl_166 ::
  Integer -> MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'8739''45'refl_166 :: Integer -> T__'8739'__20
d_'8739''45'refl_166 ~Integer
v0 = T__'8739'__20
du_'8739''45'refl_166
du_'8739''45'refl_166 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'8739''45'refl_166 :: T__'8739'__20
du_'8739''45'refl_166 = T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
du_'8739''45'reflexive_162
-- Data.Nat.Divisibility.∣-trans
d_'8739''45'trans_168 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'8739''45'trans_168 :: Integer
-> Integer
-> Integer
-> T__'8739'__20
-> T__'8739'__20
-> T__'8739'__20
d_'8739''45'trans_168 ~Integer
v0 ~Integer
v1 ~Integer
v2 T__'8739'__20
v3 T__'8739'__20
v4
  = T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'8739''45'trans_168 T__'8739'__20
v3 T__'8739'__20
v4
du_'8739''45'trans_168 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'8739''45'trans_168 :: T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'8739''45'trans_168 T__'8739'__20
v0 T__'8739'__20
v1
  = case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v0 of
      MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v2
        -> case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v1 of
             MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v4
               -> (Integer -> T__'8739'__20) -> Integer -> T__'8739'__20
forall a b. a -> b
coe
                    Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34
                    (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v4) (Integer -> Integer
forall a b. a -> b
coe Integer
v2))
             T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.∣-antisym
d_'8739''45'antisym_174 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8739''45'antisym_174 :: Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8801'__12
d_'8739''45'antisym_174 = Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.Divisibility._∣?_
d__'8739''63'__192 ::
  Integer ->
  Integer -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8739''63'__192 :: Integer -> Integer -> T_Dec_20
d__'8739''63'__192 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
             Integer
0 -> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                    ((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
                       Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
                       ((Integer -> T__'8739'__20) -> Integer -> Any
forall a b. a -> b
coe
                          Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34
                          (Integer
0 :: Integer)))
             Integer
_ -> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
      Integer
_ -> (T_Equivalence_1714 -> T_Dec_20 -> T_Dec_20)
-> Any -> T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe
             T_Equivalence_1714 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.du_map_18
             ((Integer -> Integer -> T_Equivalence_1714) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T_Equivalence_1714
du_m'37'n'8801'0'8660'n'8739'm_134 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
             (Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688
                ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
-- Data.Nat.Divisibility.∣-isPreorder
d_'8739''45'isPreorder_200 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_'8739''45'isPreorder_200 :: T_IsPreorder_70
d_'8739''45'isPreorder_200
  = (T_IsEquivalence_26
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsPreorder_70)
-> Any
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_4003
      (T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
         T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
      (\ Any
v0 Any
v1 Any
v2 -> T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
du_'8739''45'reflexive_162)
      (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> (T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'8739''45'trans_168 Any
v3 Any
v4)
-- Data.Nat.Divisibility.∣-isPartialOrder
d_'8739''45'isPartialOrder_202 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
d_'8739''45'isPartialOrder_202 :: T_IsPartialOrder_174
d_'8739''45'isPartialOrder_202
  = (T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any) -> T_IsPartialOrder_174)
-> Any -> Any -> T_IsPartialOrder_174
forall a b. a -> b
coe
      T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any) -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9853
      (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
d_'8739''45'isPreorder_200) Any
forall a. a
erased
-- Data.Nat.Divisibility.∣-preorder
d_'8739''45'preorder_204 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_'8739''45'preorder_204 :: T_Preorder_132
d_'8739''45'preorder_204
  = (T_IsPreorder_70 -> T_Preorder_132)
-> T_IsPreorder_70 -> T_Preorder_132
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2267
      T_IsPreorder_70
d_'8739''45'isPreorder_200
-- Data.Nat.Divisibility.∣-poset
d_'8739''45'poset_206 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
d_'8739''45'poset_206 :: T_Poset_314
d_'8739''45'poset_206
  = (T_IsPartialOrder_174 -> T_Poset_314)
-> T_IsPartialOrder_174 -> T_Poset_314
forall a b. a -> b
coe
      T_IsPartialOrder_174 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_6389
      T_IsPartialOrder_174
d_'8739''45'isPartialOrder_202
-- Data.Nat.Divisibility.∣-Reasoning.Base._IsRelatedTo_
d__IsRelatedTo__212 :: p -> p -> ()
d__IsRelatedTo__212 p
a0 p
a1 = ()
-- Data.Nat.Divisibility.∣-Reasoning.Base._∎
d__'8718'_214 ::
  Integer ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62
d__'8718'_214 :: Integer -> T__IsRelatedTo__62
d__'8718'_214
  = let v0 :: T_Preorder_132
v0 = T_Preorder_132
d_'8739''45'preorder_204 in
    Any -> Integer -> T__IsRelatedTo__62
forall a b. a -> b
coe
      (let v1 :: T_IsPreorder_70
v1
             = T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> T_Preorder_132
forall a b. a -> b
coe T_Preorder_132
v0) in
       Any -> Any
forall a b. a -> b
coe
         (((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__62) -> Any -> Any
forall a b. a -> b
coe
               T_IsPreorder_70 -> Any -> T__IsRelatedTo__62
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_stop_116
               (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
v1))))
-- Data.Nat.Divisibility.∣-Reasoning.Base.IsEquality
d_IsEquality_216 :: p -> p -> p -> ()
d_IsEquality_216 p
a0 p
a1 p
a2 = ()
-- Data.Nat.Divisibility.∣-Reasoning.Base.IsEquality?
d_IsEquality'63'_218 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_IsEquality'63'_218 :: Integer -> Integer -> T__IsRelatedTo__62 -> T_Dec_20
d_IsEquality'63'_218 Integer
v0 Integer
v1 T__IsRelatedTo__62
v2
  = (T__IsRelatedTo__62 -> T_Dec_20) -> T__IsRelatedTo__62 -> T_Dec_20
forall a b. a -> b
coe
      T__IsRelatedTo__62 -> T_Dec_20
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_IsEquality'63'_138
      T__IsRelatedTo__62
v2
-- Data.Nat.Divisibility.∣-Reasoning.Base.begin_
d_begin__220 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_begin__220 :: Integer -> Integer -> T__IsRelatedTo__62 -> T__'8739'__20
d_begin__220
  = let v0 :: T_Preorder_132
v0 = T_Preorder_132
d_'8739''45'preorder_204 in
    Any -> Integer -> Integer -> T__IsRelatedTo__62 -> T__'8739'__20
forall a b. a -> b
coe
      (let v1 :: T_IsPreorder_70
v1
             = T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> T_Preorder_132
forall a b. a -> b
coe T_Preorder_132
v0) in
       Any -> Any
forall a b. a -> b
coe
         (((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 -> T__IsRelatedTo__62 -> Any)
-> Any -> Any
forall a b. a -> b
coe
               T_IsPreorder_70 -> Any -> Any -> T__IsRelatedTo__62 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_start_76
               (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
v1))))
-- Data.Nat.Divisibility.∣-Reasoning.Base.begin_
d_begin__222 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_begin__222 :: Integer -> Integer -> T__IsRelatedTo__62 -> Any -> T__'8801'__12
d_begin__222 = Integer -> Integer -> T__IsRelatedTo__62 -> Any -> T__'8801'__12
forall a. a
erased
-- Data.Nat.Divisibility.∣-Reasoning.Base.equalitySubRelation
d_equalitySubRelation_224 ::
  MAlonzo.Code.Relation.Binary.Reasoning.Syntax.T_SubRelation_60
d_equalitySubRelation_224 :: T_SubRelation_60
d_equalitySubRelation_224
  = T_SubRelation_60 -> T_SubRelation_60
forall a b. a -> b
coe
      T_SubRelation_60
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_equalitySubRelation_152
-- Data.Nat.Divisibility.∣-Reasoning.Base.extractEquality
d_extractEquality_228 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T_IsEquality_122 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_extractEquality_228 :: Integer
-> Integer
-> T__IsRelatedTo__62
-> T_IsEquality_122
-> T__'8801'__12
d_extractEquality_228 = Integer
-> Integer
-> T__IsRelatedTo__62
-> T_IsEquality_122
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.Divisibility.∣-Reasoning.Base.start
d_start_234 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_start_234 :: Integer -> Integer -> T__IsRelatedTo__62 -> T__'8739'__20
d_start_234
  = let v0 :: T_Preorder_132
v0 = T_Preorder_132
d_'8739''45'preorder_204 in
    Any -> Integer -> Integer -> T__IsRelatedTo__62 -> T__'8739'__20
forall a b. a -> b
coe
      ((T_IsPreorder_70 -> Any -> Any -> T__IsRelatedTo__62 -> Any)
-> Any -> Any
forall a b. a -> b
coe
         T_IsPreorder_70 -> Any -> Any -> T__IsRelatedTo__62 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_start_76
         ((T_Preorder_132 -> T_IsPreorder_70) -> Any -> Any
forall a b. a -> b
coe
            T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> Any
forall a b. a -> b
coe T_Preorder_132
v0)))
-- Data.Nat.Divisibility.∣-Reasoning.Base.step-≡
d_step'45''8801'_246 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62
d_step'45''8801'_246 :: Integer
-> Integer
-> Integer
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
d_step'45''8801'_246
  = ((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> Any
-> Integer
-> Integer
-> Integer
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
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'_450
      ((Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> Any
v4))
-- Data.Nat.Divisibility.∣-Reasoning.Base.step-≡-∣
d_step'45''8801''45''8739'_248 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62
d_step'45''8801''45''8739'_248 :: Integer -> Integer -> T__IsRelatedTo__62 -> T__IsRelatedTo__62
d_step'45''8801''45''8739'_248 ~Integer
v0 ~Integer
v1 T__IsRelatedTo__62
v2
  = T__IsRelatedTo__62 -> T__IsRelatedTo__62
du_step'45''8801''45''8739'_248 T__IsRelatedTo__62
v2
du_step'45''8801''45''8739'_248 ::
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62
du_step'45''8801''45''8739'_248 :: T__IsRelatedTo__62 -> T__IsRelatedTo__62
du_step'45''8801''45''8739'_248 T__IsRelatedTo__62
v0 = T__IsRelatedTo__62 -> T__IsRelatedTo__62
forall a b. a -> b
coe T__IsRelatedTo__62
v0
-- Data.Nat.Divisibility.∣-Reasoning.Base.step-≡-⟨
d_step'45''8801''45''10216'_250 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62
d_step'45''8801''45''10216'_250 :: Integer
-> Integer
-> Integer
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
d_step'45''8801''45''10216'_250
  = ((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> Any
-> Integer
-> Integer
-> Integer
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
forall a b. a -> b
coe
      (Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
      ((Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> Any
v4))
-- Data.Nat.Divisibility.∣-Reasoning.Base.step-≡-⟩
d_step'45''8801''45''10217'_252 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62
d_step'45''8801''45''10217'_252 :: Integer
-> Integer
-> Integer
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
d_step'45''8801''45''10217'_252
  = ((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> Any
-> Integer
-> Integer
-> Integer
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
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 -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> Any
v4))
-- Data.Nat.Divisibility.∣-Reasoning.Base.step-≡˘
d_step'45''8801''728'_254 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62
d_step'45''8801''728'_254 :: Integer
-> Integer
-> Integer
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
d_step'45''8801''728'_254
  = ((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> Any
-> Integer
-> Integer
-> Integer
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
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''728'_452
      ((Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> Any
v4))
-- Data.Nat.Divisibility.∣-Reasoning.Base.stop
d_stop_258 ::
  Integer ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62
d_stop_258 :: Integer -> T__IsRelatedTo__62
d_stop_258
  = let v0 :: T_Preorder_132
v0 = T_Preorder_132
d_'8739''45'preorder_204 in
    Any -> Integer -> T__IsRelatedTo__62
forall a b. a -> b
coe
      ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__62) -> Any -> Any
forall a b. a -> b
coe
         T_IsPreorder_70 -> Any -> T__IsRelatedTo__62
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_stop_116
         ((T_Preorder_132 -> T_IsPreorder_70) -> Any -> Any
forall a b. a -> b
coe
            T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> Any
forall a b. a -> b
coe T_Preorder_132
v0)))
-- Data.Nat.Divisibility.∣-Reasoning.Base.≈-go
d_'8776''45'go_260 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62
d_'8776''45'go_260 :: Integer
-> Integer
-> Integer
-> T__'8801'__12
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
d_'8776''45'go_260
  = let v0 :: T_Preorder_132
v0 = T_Preorder_132
d_'8739''45'preorder_204 in
    Any
-> Integer
-> Integer
-> Integer
-> T__'8801'__12
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
forall a b. a -> b
coe
      ((T_IsPreorder_70
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__62
 -> T__IsRelatedTo__62)
-> Any -> Any
forall a b. a -> b
coe
         T_IsPreorder_70
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_'8776''45'go_106
         ((T_Preorder_132 -> T_IsPreorder_70) -> Any -> Any
forall a b. a -> b
coe
            T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> Any
forall a b. a -> b
coe T_Preorder_132
v0)))
-- Data.Nat.Divisibility.∣-Reasoning.Base.≡-go
d_'8801''45'go_262 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62
d_'8801''45'go_262 :: Integer
-> Integer
-> Integer
-> T__'8801'__12
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
d_'8801''45'go_262 ~Integer
v0 ~Integer
v1 ~Integer
v2 ~T__'8801'__12
v3 T__IsRelatedTo__62
v4 = T__IsRelatedTo__62 -> T__IsRelatedTo__62
du_'8801''45'go_262 T__IsRelatedTo__62
v4
du_'8801''45'go_262 ::
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62
du_'8801''45'go_262 :: T__IsRelatedTo__62 -> T__IsRelatedTo__62
du_'8801''45'go_262 T__IsRelatedTo__62
v0 = T__IsRelatedTo__62 -> T__IsRelatedTo__62
forall a b. a -> b
coe T__IsRelatedTo__62
v0
-- Data.Nat.Divisibility.∣-Reasoning.Base.≲-go
d_'8818''45'go_264 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62
d_'8818''45'go_264 :: Integer
-> Integer
-> Integer
-> T__'8739'__20
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
d_'8818''45'go_264
  = let v0 :: T_Preorder_132
v0 = T_Preorder_132
d_'8739''45'preorder_204 in
    Any
-> Integer
-> Integer
-> Integer
-> T__'8739'__20
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
forall a b. a -> b
coe
      ((T_IsPreorder_70
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__62
 -> T__IsRelatedTo__62)
-> Any -> Any
forall a b. a -> b
coe
         T_IsPreorder_70
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_'8818''45'go_96
         ((T_Preorder_132 -> T_IsPreorder_70) -> Any -> Any
forall a b. a -> b
coe
            T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> Any
forall a b. a -> b
coe T_Preorder_132
v0)))
-- Data.Nat.Divisibility.∣-Reasoning._.step-∣
d_step'45''8739'_278 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.T__IsRelatedTo__62
d_step'45''8739'_278 :: Integer
-> Integer
-> Integer
-> T__IsRelatedTo__62
-> T__'8739'__20
-> T__IsRelatedTo__62
d_step'45''8739'_278
  = ((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Integer
-> Integer
-> Integer
-> T__IsRelatedTo__62
-> T__'8739'__20
-> T__IsRelatedTo__62
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''8739'_332
      ((T_IsPreorder_70
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__62
 -> T__IsRelatedTo__62)
-> Any -> Any
forall a b. a -> b
coe
         T_IsPreorder_70
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_'8818''45'go_96
         (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
d_'8739''45'isPreorder_200))
-- Data.Nat.Divisibility._∣0
d__'8739'0_282 ::
  Integer -> MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d__'8739'0_282 :: Integer -> T__'8739'__20
d__'8739'0_282 ~Integer
v0 = T__'8739'__20
du__'8739'0_282
du__'8739'0_282 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du__'8739'0_282 :: T__'8739'__20
du__'8739'0_282
  = (Integer -> T__'8739'__20) -> Integer -> T__'8739'__20
forall a b. a -> b
coe
      Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 (Integer
0 :: Integer)
-- Data.Nat.Divisibility.0∣⇒≡0
d_0'8739''8658''8801'0_286 ::
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_0'8739''8658''8801'0_286 :: Integer -> T__'8739'__20 -> T__'8801'__12
d_0'8739''8658''8801'0_286 = Integer -> T__'8739'__20 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.Divisibility.1∣_
d_1'8739'__294 ::
  Integer -> MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_1'8739'__294 :: Integer -> T__'8739'__20
d_1'8739'__294 Integer
v0
  = (Integer -> T__'8739'__20) -> Integer -> T__'8739'__20
forall a b. a -> b
coe Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v0
-- Data.Nat.Divisibility.∣1⇒≡1
d_'8739'1'8658''8801'1_298 ::
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8739'1'8658''8801'1_298 :: Integer -> T__'8739'__20 -> T__'8801'__12
d_'8739'1'8658''8801'1_298 = Integer -> T__'8739'__20 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.Divisibility.n∣n
d_n'8739'n_304 ::
  Integer -> MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_n'8739'n_304 :: Integer -> T__'8739'__20
d_n'8739'n_304 ~Integer
v0 = T__'8739'__20
du_n'8739'n_304
du_n'8739'n_304 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_n'8739'n_304 :: T__'8739'__20
du_n'8739'n_304 = T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
du_'8739''45'refl_166
-- Data.Nat.Divisibility.∣m∣n⇒∣m+n
d_'8739'm'8739'n'8658''8739'm'43'n_306 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'8739'm'8739'n'8658''8739'm'43'n_306 :: Integer
-> Integer
-> Integer
-> T__'8739'__20
-> T__'8739'__20
-> T__'8739'__20
d_'8739'm'8739'n'8658''8739'm'43'n_306 ~Integer
v0 ~Integer
v1 ~Integer
v2 T__'8739'__20
v3 T__'8739'__20
v4
  = T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'8739'm'8739'n'8658''8739'm'43'n_306 T__'8739'__20
v3 T__'8739'__20
v4
du_'8739'm'8739'n'8658''8739'm'43'n_306 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'8739'm'8739'n'8658''8739'm'43'n_306 :: T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'8739'm'8739'n'8658''8739'm'43'n_306 T__'8739'__20
v0 T__'8739'__20
v1
  = case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v0 of
      MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v2
        -> case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v1 of
             MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v4
               -> (Integer -> T__'8739'__20) -> Integer -> T__'8739'__20
forall a b. a -> b
coe
                    Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34
                    (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
             T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.∣m+n∣m⇒∣n
d_'8739'm'43'n'8739'm'8658''8739'n_312 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'8739'm'43'n'8739'm'8658''8739'n_312 :: Integer
-> Integer
-> Integer
-> T__'8739'__20
-> T__'8739'__20
-> T__'8739'__20
d_'8739'm'43'n'8739'm'8658''8739'n_312 ~Integer
v0 ~Integer
v1 ~Integer
v2 T__'8739'__20
v3 T__'8739'__20
v4
  = T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'8739'm'43'n'8739'm'8658''8739'n_312 T__'8739'__20
v3 T__'8739'__20
v4
du_'8739'm'43'n'8739'm'8658''8739'n_312 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'8739'm'43'n'8739'm'8658''8739'n_312 :: T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'8739'm'43'n'8739'm'8658''8739'n_312 T__'8739'__20
v0 T__'8739'__20
v1
  = case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v0 of
      MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v2
        -> case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v1 of
             MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v4
               -> (Integer -> T__'8739'__20) -> Any -> T__'8739'__20
forall a b. a -> b
coe
                    Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34
                    ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v2 Integer
v4)
             T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.n∣m*n
d_n'8739'm'42'n_338 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_n'8739'm'42'n_338 :: Integer -> Integer -> T__'8739'__20
d_n'8739'm'42'n_338 Integer
v0 ~Integer
v1 = Integer -> T__'8739'__20
du_n'8739'm'42'n_338 Integer
v0
du_n'8739'm'42'n_338 ::
  Integer -> MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_n'8739'm'42'n_338 :: Integer -> T__'8739'__20
du_n'8739'm'42'n_338 Integer
v0
  = (Integer -> T__'8739'__20) -> Integer -> T__'8739'__20
forall a b. a -> b
coe Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v0
-- Data.Nat.Divisibility.m∣m*n
d_m'8739'm'42'n_346 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_m'8739'm'42'n_346 :: Integer -> Integer -> T__'8739'__20
d_m'8739'm'42'n_346 ~Integer
v0 Integer
v1 = Integer -> T__'8739'__20
du_m'8739'm'42'n_346 Integer
v1
du_m'8739'm'42'n_346 ::
  Integer -> MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_m'8739'm'42'n_346 :: Integer -> T__'8739'__20
du_m'8739'm'42'n_346 Integer
v0
  = (Integer -> T__'8739'__20) -> Integer -> T__'8739'__20
forall a b. a -> b
coe Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v0
-- Data.Nat.Divisibility.n∣m*n*o
d_n'8739'm'42'n'42'o_356 ::
  Integer ->
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_n'8739'm'42'n'42'o_356 :: Integer -> Integer -> Integer -> T__'8739'__20
d_n'8739'm'42'n'42'o_356 Integer
v0 ~Integer
v1 Integer
v2
  = Integer -> Integer -> T__'8739'__20
du_n'8739'm'42'n'42'o_356 Integer
v0 Integer
v2
du_n'8739'm'42'n'42'o_356 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_n'8739'm'42'n'42'o_356 :: Integer -> Integer -> T__'8739'__20
du_n'8739'm'42'n'42'o_356 Integer
v0 Integer
v1
  = (T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20)
-> Any -> Any -> T__'8739'__20
forall a b. a -> b
coe
      T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'8739''45'trans_168 ((Integer -> T__'8739'__20) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8739'__20
du_n'8739'm'42'n_338 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
      ((Integer -> T__'8739'__20) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8739'__20
du_m'8739'm'42'n_346 (Integer -> Any
forall a b. a -> b
coe Integer
v1))
-- Data.Nat.Divisibility.∣m⇒∣m*n
d_'8739'm'8658''8739'm'42'n_364 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'8739'm'8658''8739'm'42'n_364 :: Integer -> Integer -> Integer -> T__'8739'__20 -> T__'8739'__20
d_'8739'm'8658''8739'm'42'n_364 ~Integer
v0 ~Integer
v1 Integer
v2 T__'8739'__20
v3
  = Integer -> T__'8739'__20 -> T__'8739'__20
du_'8739'm'8658''8739'm'42'n_364 Integer
v2 T__'8739'__20
v3
du_'8739'm'8658''8739'm'42'n_364 ::
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'8739'm'8658''8739'm'42'n_364 :: Integer -> T__'8739'__20 -> T__'8739'__20
du_'8739'm'8658''8739'm'42'n_364 Integer
v0 T__'8739'__20
v1
  = case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v1 of
      MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v2
        -> (T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20)
-> Any -> Any -> T__'8739'__20
forall a b. a -> b
coe
             T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'8739''45'trans_168 ((Integer -> T__'8739'__20) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8739'__20
du_n'8739'm'42'n_338 (Integer -> Any
forall a b. a -> b
coe Integer
v2))
             ((Integer -> T__'8739'__20) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8739'__20
du_m'8739'm'42'n_346 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
      T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.∣n⇒∣m*n
d_'8739'n'8658''8739'm'42'n_374 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'8739'n'8658''8739'm'42'n_374 :: Integer -> Integer -> Integer -> T__'8739'__20 -> T__'8739'__20
d_'8739'n'8658''8739'm'42'n_374 ~Integer
v0 Integer
v1 ~Integer
v2
  = Integer -> T__'8739'__20 -> T__'8739'__20
du_'8739'n'8658''8739'm'42'n_374 Integer
v1
du_'8739'n'8658''8739'm'42'n_374 ::
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'8739'n'8658''8739'm'42'n_374 :: Integer -> T__'8739'__20 -> T__'8739'__20
du_'8739'n'8658''8739'm'42'n_374 Integer
v0
  = (Integer -> T__'8739'__20 -> T__'8739'__20)
-> Any -> T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe Integer -> T__'8739'__20 -> T__'8739'__20
du_'8739'm'8658''8739'm'42'n_364 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
-- Data.Nat.Divisibility.m*n∣⇒m∣
d_m'42'n'8739''8658'm'8739'_388 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_m'42'n'8739''8658'm'8739'_388 :: Integer -> Integer -> Integer -> T__'8739'__20 -> T__'8739'__20
d_m'42'n'8739''8658'm'8739'_388 ~Integer
v0 ~Integer
v1 Integer
v2 T__'8739'__20
v3
  = Integer -> T__'8739'__20 -> T__'8739'__20
du_m'42'n'8739''8658'm'8739'_388 Integer
v2 T__'8739'__20
v3
du_m'42'n'8739''8658'm'8739'_388 ::
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_m'42'n'8739''8658'm'8739'_388 :: Integer -> T__'8739'__20 -> T__'8739'__20
du_m'42'n'8739''8658'm'8739'_388 Integer
v0 T__'8739'__20
v1
  = case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v1 of
      MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v2
        -> (Integer -> T__'8739'__20 -> T__'8739'__20)
-> Integer -> Any -> T__'8739'__20
forall a b. a -> b
coe
             Integer -> T__'8739'__20 -> T__'8739'__20
du_'8739'n'8658''8739'm'42'n_374 Integer
v2
             ((Integer -> T__'8739'__20) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8739'__20
du_m'8739'm'42'n_346 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
      T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.m*n∣⇒n∣
d_m'42'n'8739''8658'n'8739'_400 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_m'42'n'8739''8658'n'8739'_400 :: Integer -> Integer -> Integer -> T__'8739'__20 -> T__'8739'__20
d_m'42'n'8739''8658'n'8739'_400 ~Integer
v0 Integer
v1 ~Integer
v2
  = Integer -> T__'8739'__20 -> T__'8739'__20
du_m'42'n'8739''8658'n'8739'_400 Integer
v1
du_m'42'n'8739''8658'n'8739'_400 ::
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_m'42'n'8739''8658'n'8739'_400 :: Integer -> T__'8739'__20 -> T__'8739'__20
du_m'42'n'8739''8658'n'8739'_400 Integer
v0
  = (Integer -> T__'8739'__20 -> T__'8739'__20)
-> Any -> T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe Integer -> T__'8739'__20 -> T__'8739'__20
du_m'42'n'8739''8658'm'8739'_388 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
-- Data.Nat.Divisibility.*-pres-∣
d_'42''45'pres'45''8739'_410 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'42''45'pres'45''8739'_410 :: Integer
-> Integer
-> Integer
-> Integer
-> T__'8739'__20
-> T__'8739'__20
-> T__'8739'__20
d_'42''45'pres'45''8739'_410 ~Integer
v0 ~Integer
v1 ~Integer
v2 ~Integer
v3 T__'8739'__20
v4 T__'8739'__20
v5
  = T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'42''45'pres'45''8739'_410 T__'8739'__20
v4 T__'8739'__20
v5
du_'42''45'pres'45''8739'_410 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'42''45'pres'45''8739'_410 :: T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'42''45'pres'45''8739'_410 T__'8739'__20
v0 T__'8739'__20
v1
  = case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v0 of
      MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v2
        -> case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v1 of
             MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v4
               -> (Integer -> T__'8739'__20) -> Integer -> T__'8739'__20
forall a b. a -> b
coe
                    Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34
                    (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
             T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.*-monoʳ-∣
d_'42''45'mono'691''45''8739'_426 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'42''45'mono'691''45''8739'_426 :: Integer -> Integer -> Integer -> T__'8739'__20 -> T__'8739'__20
d_'42''45'mono'691''45''8739'_426 ~Integer
v0 ~Integer
v1 ~Integer
v2
  = T__'8739'__20 -> T__'8739'__20
du_'42''45'mono'691''45''8739'_426
du_'42''45'mono'691''45''8739'_426 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'42''45'mono'691''45''8739'_426 :: T__'8739'__20 -> T__'8739'__20
du_'42''45'mono'691''45''8739'_426
  = (T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20)
-> Any -> T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'42''45'pres'45''8739'_410 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
du_'8739''45'refl_166)
-- Data.Nat.Divisibility.*-monoˡ-∣
d_'42''45'mono'737''45''8739'_432 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'42''45'mono'737''45''8739'_432 :: Integer -> Integer -> Integer -> T__'8739'__20 -> T__'8739'__20
d_'42''45'mono'737''45''8739'_432 ~Integer
v0 ~Integer
v1 ~Integer
v2 T__'8739'__20
v3
  = T__'8739'__20 -> T__'8739'__20
du_'42''45'mono'737''45''8739'_432 T__'8739'__20
v3
du_'42''45'mono'737''45''8739'_432 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'42''45'mono'737''45''8739'_432 :: T__'8739'__20 -> T__'8739'__20
du_'42''45'mono'737''45''8739'_432 T__'8739'__20
v0
  = (T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20)
-> Any -> Any -> T__'8739'__20
forall a b. a -> b
coe
      T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'42''45'pres'45''8739'_410 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v0) (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
du_'8739''45'refl_166)
-- Data.Nat.Divisibility.*-cancelˡ-∣
d_'42''45'cancel'737''45''8739'_440 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'42''45'cancel'737''45''8739'_440 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
d_'42''45'cancel'737''45''8739'_440 ~Integer
v0 ~Integer
v1 ~Integer
v2 ~T_NonZero_112
v3 T__'8739'__20
v4
  = T__'8739'__20 -> T__'8739'__20
du_'42''45'cancel'737''45''8739'_440 T__'8739'__20
v4
du_'42''45'cancel'737''45''8739'_440 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'42''45'cancel'737''45''8739'_440 :: T__'8739'__20 -> T__'8739'__20
du_'42''45'cancel'737''45''8739'_440 T__'8739'__20
v0
  = (Integer -> T__'8739'__20) -> Any -> T__'8739'__20
forall a b. a -> b
coe
      Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34
      ((T__'8739'__20 -> Integer) -> Any -> Any
forall a b. a -> b
coe T__'8739'__20 -> Integer
du_q_454 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v0))
-- Data.Nat.Divisibility._.q
d_q_454 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 -> Integer
d_q_454 :: Integer
-> Integer -> Integer -> T_NonZero_112 -> T__'8739'__20 -> Integer
d_q_454 ~Integer
v0 ~Integer
v1 ~Integer
v2 ~T_NonZero_112
v3 T__'8739'__20
v4 = T__'8739'__20 -> Integer
du_q_454 T__'8739'__20
v4
du_q_454 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 -> Integer
du_q_454 :: T__'8739'__20 -> Integer
du_q_454 T__'8739'__20
v0
  = (T__'8739'__20 -> Integer) -> Any -> Integer
forall a b. a -> b
coe
      T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v0)
-- Data.Nat.Divisibility.*-cancelʳ-∣
d_'42''45'cancel'691''45''8739'_462 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'42''45'cancel'691''45''8739'_462 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
d_'42''45'cancel'691''45''8739'_462 ~Integer
v0 ~Integer
v1 ~Integer
v2 ~T_NonZero_112
v3
  = T__'8739'__20 -> T__'8739'__20
du_'42''45'cancel'691''45''8739'_462
du_'42''45'cancel'691''45''8739'_462 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'42''45'cancel'691''45''8739'_462 :: T__'8739'__20 -> T__'8739'__20
du_'42''45'cancel'691''45''8739'_462
  = (T__'8739'__20 -> T__'8739'__20) -> T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20 -> T__'8739'__20
du_'42''45'cancel'737''45''8739'_440
-- Data.Nat.Divisibility.∣m∸n∣n⇒∣m
d_'8739'm'8760'n'8739'n'8658''8739'm_480 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'8739'm'8760'n'8739'n'8658''8739'm_480 :: Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8739'__20
-> T__'8739'__20
-> T__'8739'__20
d_'8739'm'8760'n'8739'n'8658''8739'm_480 ~Integer
v0 ~Integer
v1 ~Integer
v2 ~T__'8804'__22
v3 T__'8739'__20
v4 T__'8739'__20
v5
  = T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'8739'm'8760'n'8739'n'8658''8739'm_480 T__'8739'__20
v4 T__'8739'__20
v5
du_'8739'm'8760'n'8739'n'8658''8739'm_480 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'8739'm'8760'n'8739'n'8658''8739'm_480 :: T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'8739'm'8760'n'8739'n'8658''8739'm_480 T__'8739'__20
v0 T__'8739'__20
v1
  = case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v0 of
      MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v2
        -> case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v1 of
             MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v4
               -> (Integer -> T__'8739'__20) -> Integer -> T__'8739'__20
forall a b. a -> b
coe
                    Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34
                    (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
             T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.m/n∣m
d_m'47'n'8739'm_504 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_m'47'n'8739'm_504 :: Integer
-> Integer -> T_NonZero_112 -> T__'8739'__20 -> T__'8739'__20
d_m'47'n'8739'm_504 Integer
v0 Integer
v1 ~T_NonZero_112
v2 T__'8739'__20
v3 = Integer -> Integer -> T__'8739'__20 -> T__'8739'__20
du_m'47'n'8739'm_504 Integer
v0 Integer
v1 T__'8739'__20
v3
du_m'47'n'8739'm_504 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_m'47'n'8739'm_504 :: Integer -> Integer -> T__'8739'__20 -> T__'8739'__20
du_m'47'n'8739'm_504 Integer
v0 Integer
v1 T__'8739'__20
v2
  = let v3 :: T_IsPreorder_70
v3 = T_IsPreorder_70
d_'8739''45'isPreorder_200 in
    Any -> T__'8739'__20
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 -> T__IsRelatedTo__62 -> Any)
-> Any -> Any
forall a b. a -> b
coe
            T_IsPreorder_70 -> Any -> Any -> T__IsRelatedTo__62 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_start_76
            (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
v3))
         ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) Integer
v1
         (((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
            (Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
            (\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 -> Any
v8)
            ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
            (T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v2)) Integer
v1
            (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
               (Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8739'_332
               ((T_IsPreorder_70
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__62
 -> T__IsRelatedTo__62)
-> Any -> Any
forall a b. a -> b
coe
                  T_IsPreorder_70
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_'8818''45'go_96
                  (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
d_'8739''45'isPreorder_200))
               (T__'8739'__20 -> Integer
MAlonzo.Code.Data.Nat.Divisibility.Core.d_quotient_30 (T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v2)) Integer
v1
               Integer
v1
               (let v4 :: T_IsPreorder_70
v4 = T_IsPreorder_70
d_'8739''45'isPreorder_200 in
                Any -> Any
forall a b. a -> b
coe
                  (((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__62) -> Any -> Any
forall a b. a -> b
coe
                        T_IsPreorder_70 -> Any -> T__IsRelatedTo__62
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_stop_116
                        (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
v4))
                     (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
               ((Integer -> T__'8739'__20) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8739'__20
du_quotient'45''8739'_46 (Integer -> Any
forall a b. a -> b
coe Integer
v0)))
            Any
forall a. a
erased))
-- Data.Nat.Divisibility.m*n∣o⇒m∣o/n
d_m'42'n'8739'o'8658'm'8739'o'47'n_522 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_m'42'n'8739'o'8658'm'8739'o'47'n_522 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
d_m'42'n'8739'o'8658'm'8739'o'47'n_522 ~Integer
v0 ~Integer
v1 ~Integer
v2 ~T_NonZero_112
v3 T__'8739'__20
v4
  = T__'8739'__20 -> T__'8739'__20
du_m'42'n'8739'o'8658'm'8739'o'47'n_522 T__'8739'__20
v4
du_m'42'n'8739'o'8658'm'8739'o'47'n_522 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_m'42'n'8739'o'8658'm'8739'o'47'n_522 :: T__'8739'__20 -> T__'8739'__20
du_m'42'n'8739'o'8658'm'8739'o'47'n_522 T__'8739'__20
v0 = T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v0
-- Data.Nat.Divisibility.m*n∣o⇒n∣o/m
d_m'42'n'8739'o'8658'n'8739'o'47'm_542 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_m'42'n'8739'o'8658'n'8739'o'47'm_542 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
d_m'42'n'8739'o'8658'n'8739'o'47'm_542 ~Integer
v0 ~Integer
v1 ~Integer
v2 ~T_NonZero_112
v3 T__'8739'__20
v4
  = T__'8739'__20 -> T__'8739'__20
du_m'42'n'8739'o'8658'n'8739'o'47'm_542 T__'8739'__20
v4
du_m'42'n'8739'o'8658'n'8739'o'47'm_542 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_m'42'n'8739'o'8658'n'8739'o'47'm_542 :: T__'8739'__20 -> T__'8739'__20
du_m'42'n'8739'o'8658'n'8739'o'47'm_542 T__'8739'__20
v0 = T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v0
-- Data.Nat.Divisibility.m∣n/o⇒m*o∣n
d_m'8739'n'47'o'8658'm'42'o'8739'n_554 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_m'8739'n'47'o'8658'm'42'o'8739'n_554 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
-> T__'8739'__20
d_m'8739'n'47'o'8658'm'42'o'8739'n_554 Integer
v0 ~Integer
v1 Integer
v2 ~T_NonZero_112
v3 T__'8739'__20
v4 T__'8739'__20
v5
  = Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_m'8739'n'47'o'8658'm'42'o'8739'n_554 Integer
v0 Integer
v2 T__'8739'__20
v4 T__'8739'__20
v5
du_m'8739'n'47'o'8658'm'42'o'8739'n_554 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_m'8739'n'47'o'8658'm'42'o'8739'n_554 :: Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_m'8739'n'47'o'8658'm'42'o'8739'n_554 Integer
v0 Integer
v1 T__'8739'__20
v2 T__'8739'__20
v3
  = case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v2 of
      MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v4
        -> let v6 :: T_IsPreorder_70
v6 = T_IsPreorder_70
d_'8739''45'isPreorder_200 in
           Any -> T__'8739'__20
forall a b. a -> b
coe
             (((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Integer -> 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 -> T__IsRelatedTo__62 -> Any)
-> Any -> Any
forall a b. a -> b
coe
                   T_IsPreorder_70 -> Any -> Any -> T__IsRelatedTo__62 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_start_76
                   (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
v6))
                (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v4) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
                   (Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8739'_332
                   ((T_IsPreorder_70
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__62
 -> T__IsRelatedTo__62)
-> Any -> Any
forall a b. a -> b
coe
                      T_IsPreorder_70
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_'8818''45'go_96
                      (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
d_'8739''45'isPreorder_200))
                   (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v4) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                   (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v4) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                   (let v7 :: T_IsPreorder_70
v7 = T_IsPreorder_70
d_'8739''45'isPreorder_200 in
                    Any -> Any
forall a b. a -> b
coe
                      (((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__62) -> Any -> Any
forall a b. a -> b
coe
                            T_IsPreorder_70 -> Any -> T__IsRelatedTo__62
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_stop_116
                            (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
v7))
                         ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v0))))
                   ((T__'8739'__20 -> T__'8739'__20) -> Any -> Any
forall a b. a -> b
coe T__'8739'__20 -> T__'8739'__20
du_'42''45'mono'737''45''8739'_432 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v3))))
      T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.m∣n/o⇒o*m∣n
d_m'8739'n'47'o'8658'o'42'm'8739'n_574 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_m'8739'n'47'o'8658'o'42'm'8739'n_574 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
-> T__'8739'__20
d_m'8739'n'47'o'8658'o'42'm'8739'n_574 Integer
v0 ~Integer
v1 Integer
v2 ~T_NonZero_112
v3
  = Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_m'8739'n'47'o'8658'o'42'm'8739'n_574 Integer
v0 Integer
v2
du_m'8739'n'47'o'8658'o'42'm'8739'n_574 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_m'8739'n'47'o'8658'o'42'm'8739'n_574 :: Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_m'8739'n'47'o'8658'o'42'm'8739'n_574 Integer
v0 Integer
v1
  = (Integer
 -> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20)
-> Any -> Any -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_m'8739'n'47'o'8658'm'42'o'8739'n_554 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Nat.Divisibility.m/n∣o⇒m∣o*n
d_m'47'n'8739'o'8658'm'8739'o'42'n_586 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_m'47'n'8739'o'8658'm'8739'o'42'n_586 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
-> T__'8739'__20
d_m'47'n'8739'o'8658'm'8739'o'42'n_586 Integer
v0 ~Integer
v1 Integer
v2 ~T_NonZero_112
v3 T__'8739'__20
v4 T__'8739'__20
v5
  = Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_m'47'n'8739'o'8658'm'8739'o'42'n_586 Integer
v0 Integer
v2 T__'8739'__20
v4 T__'8739'__20
v5
du_m'47'n'8739'o'8658'm'8739'o'42'n_586 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_m'47'n'8739'o'8658'm'8739'o'42'n_586 :: Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_m'47'n'8739'o'8658'm'8739'o'42'n_586 Integer
v0 Integer
v1 T__'8739'__20
v2 T__'8739'__20
v3
  = case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v2 of
      MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v4
        -> let v6 :: T_IsPreorder_70
v6 = T_IsPreorder_70
d_'8739''45'isPreorder_200 in
           Any -> T__'8739'__20
forall a b. a -> b
coe
             (((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Integer -> 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 -> T__IsRelatedTo__62 -> Any)
-> Any -> Any
forall a b. a -> b
coe
                   T_IsPreorder_70 -> Any -> Any -> T__IsRelatedTo__62 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_start_76
                   (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
v6))
                (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v4) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                (((Any -> Any -> Any -> Any -> Any -> Any)
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
                   (Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8739'_332
                   ((T_IsPreorder_70
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__62
 -> T__IsRelatedTo__62)
-> Any -> Any
forall a b. a -> b
coe
                      T_IsPreorder_70
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_'8818''45'go_96
                      (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
d_'8739''45'isPreorder_200))
                   (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v4) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                   (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                   (let v7 :: T_IsPreorder_70
v7 = T_IsPreorder_70
d_'8739''45'isPreorder_200 in
                    Any -> Any
forall a b. a -> b
coe
                      (((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__62) -> Any -> Any
forall a b. a -> b
coe
                            T_IsPreorder_70 -> Any -> T__IsRelatedTo__62
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_stop_116
                            (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
v7))
                         ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0))))
                   ((T__'8739'__20 -> T__'8739'__20) -> Any -> Any
forall a b. a -> b
coe T__'8739'__20 -> T__'8739'__20
du_'42''45'mono'737''45''8739'_432 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v3))))
      T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.m∣n*o⇒m/n∣o
d_m'8739'n'42'o'8658'm'47'n'8739'o_606 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_m'8739'n'42'o'8658'm'47'n'8739'o_606 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
-> T__'8739'__20
d_m'8739'n'42'o'8658'm'47'n'8739'o_606 Integer
v0 ~Integer
v1 Integer
v2 ~T_NonZero_112
v3 T__'8739'__20
v4 T__'8739'__20
v5
  = Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_m'8739'n'42'o'8658'm'47'n'8739'o_606 Integer
v0 Integer
v2 T__'8739'__20
v4 T__'8739'__20
v5
du_m'8739'n'42'o'8658'm'47'n'8739'o_606 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_m'8739'n'42'o'8658'm'47'n'8739'o_606 :: Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_m'8739'n'42'o'8658'm'47'n'8739'o_606 Integer
v0 Integer
v1 T__'8739'__20
v2 T__'8739'__20
v3
  = case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v2 of
      MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v4
        -> let v6 :: T_IsPreorder_70
v6 = T_IsPreorder_70
d_'8739''45'isPreorder_200 in
           Any -> T__'8739'__20
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 -> T__IsRelatedTo__62 -> Any)
-> Any -> Any
forall a b. a -> b
coe
                   T_IsPreorder_70 -> Any -> Any -> T__IsRelatedTo__62 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_start_76
                   (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
v6))
                ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                   Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314
                   ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                Integer
v1
                (((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
 -> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                   (Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
                   (\ Any
v7 Any
v8 Any
v9 Any
v10 Any
v11 -> Any
v11)
                   ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                      Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314
                      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                   Integer
v4 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''8739'_332
                      ((T_IsPreorder_70
 -> Any
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__62
 -> T__IsRelatedTo__62)
-> Any -> Any
forall a b. a -> b
coe
                         T_IsPreorder_70
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_'8818''45'go_96
                         (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
d_'8739''45'isPreorder_200))
                      Integer
v4 Integer
v1 Integer
v1
                      (let v7 :: T_IsPreorder_70
v7 = T_IsPreorder_70
d_'8739''45'isPreorder_200 in
                       Any -> Any
forall a b. a -> b
coe
                         (((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__62) -> Any -> Any
forall a b. a -> b
coe
                               T_IsPreorder_70 -> Any -> T__IsRelatedTo__62
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double.du_stop_116
                               (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
v7))
                            (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
                      ((T__'8739'__20 -> T__'8739'__20) -> T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20 -> T__'8739'__20
du_'42''45'cancel'691''45''8739'_462 T__'8739'__20
v3))
                   Any
forall a. a
erased))
      T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.∣n∣m%n⇒∣m
d_'8739'n'8739'm'37'n'8658''8739'm_624 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'8739'n'8739'm'37'n'8658''8739'm_624 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
-> T__'8739'__20
d_'8739'n'8739'm'37'n'8658''8739'm_624 ~Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 T__'8739'__20
v4 T__'8739'__20
v5
  = Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'8739'n'8739'm'37'n'8658''8739'm_624 Integer
v1 Integer
v2 T__'8739'__20
v4 T__'8739'__20
v5
du_'8739'n'8739'm'37'n'8658''8739'm_624 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'8739'n'8739'm'37'n'8658''8739'm_624 :: Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'8739'n'8739'm'37'n'8658''8739'm_624 Integer
v0 Integer
v1 T__'8739'__20
v2 T__'8739'__20
v3
  = case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v2 of
      MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v4
        -> case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v3 of
             MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v6
               -> (Integer -> T__'8739'__20) -> Integer -> T__'8739'__20
forall a b. a -> b
coe
                    Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34
                    (Integer -> Integer -> Integer
addInt
                       ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
                          Integer -> Integer -> Integer
mulInt
                          ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                             Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v1)
                             ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v0)))
                          (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                       (Integer -> Integer
forall a b. a -> b
coe Integer
v6))
             T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.%-presˡ-∣
d_'37''45'pres'737''45''8739'_648 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_'37''45'pres'737''45''8739'_648 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
-> T__'8739'__20
d_'37''45'pres'737''45''8739'_648 Integer
v0 Integer
v1 ~Integer
v2 ~T_NonZero_112
v3 T__'8739'__20
v4 T__'8739'__20
v5
  = Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'37''45'pres'737''45''8739'_648 Integer
v0 Integer
v1 T__'8739'__20
v4 T__'8739'__20
v5
du_'37''45'pres'737''45''8739'_648 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_'37''45'pres'737''45''8739'_648 :: Integer
-> Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'37''45'pres'737''45''8739'_648 Integer
v0 Integer
v1 T__'8739'__20
v2 T__'8739'__20
v3
  = case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v2 of
      MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v4
        -> case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v3 of
             MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34 Integer
v6
               -> (Integer -> T__'8739'__20) -> Any -> T__'8739'__20
forall a b. a -> b
coe
                    Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34
                    ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                       Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v4
                       (Integer -> Integer -> Integer
mulInt
                          ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
                             Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314
                             ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v1)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                          (Integer -> Integer
forall a b. a -> b
coe Integer
v6)))
             T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.m≤n⇒m!∣n!
d_m'8804'n'8658'm'33''8739'n'33'_670 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_m'8804'n'8658'm'33''8739'n'33'_670 :: Integer -> Integer -> T__'8804'__22 -> T__'8739'__20
d_m'8804'n'8658'm'33''8739'n'33'_670 ~Integer
v0 Integer
v1 T__'8804'__22
v2
  = Integer -> T__'8804'__22 -> T__'8739'__20
du_m'8804'n'8658'm'33''8739'n'33'_670 Integer
v1 T__'8804'__22
v2
du_m'8804'n'8658'm'33''8739'n'33'_670 ::
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_m'8804'n'8658'm'33''8739'n'33'_670 :: Integer -> T__'8804'__22 -> T__'8739'__20
du_m'8804'n'8658'm'33''8739'n'33'_670 Integer
v0 T__'8804'__22
v1
  = (Integer -> T__'8804''8242'__338 -> T__'8739'__20)
-> Any -> Any -> T__'8739'__20
forall a b. a -> b
coe
      Integer -> T__'8804''8242'__338 -> T__'8739'__20
du_help_678 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
      ((Integer -> T__'8804'__22 -> T__'8804''8242'__338)
-> Any -> Any -> Any
forall a b. a -> b
coe
         Integer -> T__'8804'__22 -> T__'8804''8242'__338
MAlonzo.Code.Data.Nat.Properties.du_'8804''8658''8804''8242'_6128
         (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v1))
-- Data.Nat.Divisibility._.help
d_help_678 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804''8242'__338 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_help_678 :: Integer
-> Integer
-> T__'8804'__22
-> Integer
-> Integer
-> T__'8804''8242'__338
-> T__'8739'__20
d_help_678 ~Integer
v0 ~Integer
v1 ~T__'8804'__22
v2 ~Integer
v3 Integer
v4 T__'8804''8242'__338
v5 = Integer -> T__'8804''8242'__338 -> T__'8739'__20
du_help_678 Integer
v4 T__'8804''8242'__338
v5
du_help_678 ::
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804''8242'__338 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_help_678 :: Integer -> T__'8804''8242'__338 -> T__'8739'__20
du_help_678 Integer
v0 T__'8804''8242'__338
v1
  = case T__'8804''8242'__338 -> T__'8804''8242'__338
forall a b. a -> b
coe T__'8804''8242'__338
v1 of
      T__'8804''8242'__338
MAlonzo.Code.Data.Nat.Base.C_'8804''8242''45'refl_342
        -> T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
du_'8739''45'refl_166
      MAlonzo.Code.Data.Nat.Base.C_'8804''8242''45'step_348 T__'8804''8242'__338
v3
        -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T__'8739'__20
forall a b. a -> b
coe
             ((Integer -> T__'8739'__20 -> T__'8739'__20)
-> Integer -> Any -> Any
forall a b. a -> b
coe
                Integer -> T__'8739'__20 -> T__'8739'__20
du_'8739'n'8658''8739'm'42'n_374 Integer
v0
                ((Integer -> T__'8804''8242'__338 -> T__'8739'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8804''8242'__338 -> T__'8739'__20
du_help_678 (Integer -> Any
forall a b. a -> b
coe Integer
v4) (T__'8804''8242'__338 -> Any
forall a b. a -> b
coe T__'8804''8242'__338
v3)))
      T__'8804''8242'__338
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.hasNonTrivialDivisor-≢
d_hasNonTrivialDivisor'45''8802'_684 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T_NonTrivial_152 ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__HasNonTrivialDivisorLessThan__50
d_hasNonTrivialDivisor'45''8802'_684 :: Integer
-> Integer
-> T_NonTrivial_152
-> T_NonZero_112
-> (T__'8801'__12 -> T_Irrelevant_20)
-> T__'8739'__20
-> T__HasNonTrivialDivisorLessThan__50
d_hasNonTrivialDivisor'45''8802'_684 Integer
v0 Integer
v1 ~T_NonTrivial_152
v2 ~T_NonZero_112
v3 ~T__'8801'__12 -> T_Irrelevant_20
v4 T__'8739'__20
v5
  = Integer
-> Integer -> T__'8739'__20 -> T__HasNonTrivialDivisorLessThan__50
du_hasNonTrivialDivisor'45''8802'_684 Integer
v0 Integer
v1 T__'8739'__20
v5
du_hasNonTrivialDivisor'45''8802'_684 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__HasNonTrivialDivisorLessThan__50
du_hasNonTrivialDivisor'45''8802'_684 :: Integer
-> Integer -> T__'8739'__20 -> T__HasNonTrivialDivisorLessThan__50
du_hasNonTrivialDivisor'45''8802'_684 Integer
v0 Integer
v1 T__'8739'__20
v2
  = (Integer
 -> T__'8804'__22
 -> T__'8739'__20
 -> T__HasNonTrivialDivisorLessThan__50)
-> Integer
-> Any
-> T__'8739'__20
-> T__HasNonTrivialDivisorLessThan__50
forall a b. a -> b
coe
      Integer
-> T__'8804'__22
-> T__'8739'__20
-> T__HasNonTrivialDivisorLessThan__50
MAlonzo.Code.Data.Nat.Divisibility.Core.C_hasNonTrivialDivisor_72
      Integer
v0
      ((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_'8804''8743''8802''8658''60'_2918
         (Integer -> Any
forall a b. a -> b
coe Integer
v1) ((Integer -> T__'8739'__20 -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8739'__20 -> T__'8804'__22
du_'8739''8658''8804'_142 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v2)))
      T__'8739'__20
v2
-- Data.Nat.Divisibility.hasNonTrivialDivisor-∣
d_hasNonTrivialDivisor'45''8739'_690 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__HasNonTrivialDivisorLessThan__50 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__HasNonTrivialDivisorLessThan__50
d_hasNonTrivialDivisor'45''8739'_690 :: Integer
-> Integer
-> Integer
-> T__HasNonTrivialDivisorLessThan__50
-> T__'8739'__20
-> T__HasNonTrivialDivisorLessThan__50
d_hasNonTrivialDivisor'45''8739'_690 ~Integer
v0 ~Integer
v1 ~Integer
v2 T__HasNonTrivialDivisorLessThan__50
v3 T__'8739'__20
v4
  = T__HasNonTrivialDivisorLessThan__50
-> T__'8739'__20 -> T__HasNonTrivialDivisorLessThan__50
du_hasNonTrivialDivisor'45''8739'_690 T__HasNonTrivialDivisorLessThan__50
v3 T__'8739'__20
v4
du_hasNonTrivialDivisor'45''8739'_690 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__HasNonTrivialDivisorLessThan__50 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__HasNonTrivialDivisorLessThan__50
du_hasNonTrivialDivisor'45''8739'_690 :: T__HasNonTrivialDivisorLessThan__50
-> T__'8739'__20 -> T__HasNonTrivialDivisorLessThan__50
du_hasNonTrivialDivisor'45''8739'_690 T__HasNonTrivialDivisorLessThan__50
v0 T__'8739'__20
v1
  = case T__HasNonTrivialDivisorLessThan__50
-> T__HasNonTrivialDivisorLessThan__50
forall a b. a -> b
coe T__HasNonTrivialDivisorLessThan__50
v0 of
      MAlonzo.Code.Data.Nat.Divisibility.Core.C_hasNonTrivialDivisor_72 Integer
v2 T__'8804'__22
v4 T__'8739'__20
v5
        -> (Integer
 -> T__'8804'__22
 -> T__'8739'__20
 -> T__HasNonTrivialDivisorLessThan__50)
-> Integer
-> T__'8804'__22
-> Any
-> T__HasNonTrivialDivisorLessThan__50
forall a b. a -> b
coe
             Integer
-> T__'8804'__22
-> T__'8739'__20
-> T__HasNonTrivialDivisorLessThan__50
MAlonzo.Code.Data.Nat.Divisibility.Core.C_hasNonTrivialDivisor_72
             Integer
v2 T__'8804'__22
v4 ((T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'8739''45'trans_168 (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v5) (T__'8739'__20 -> Any
forall a b. a -> b
coe T__'8739'__20
v1))
      T__HasNonTrivialDivisorLessThan__50
_ -> T__HasNonTrivialDivisorLessThan__50
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.hasNonTrivialDivisor-≤
d_hasNonTrivialDivisor'45''8804'_698 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__HasNonTrivialDivisorLessThan__50 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__HasNonTrivialDivisorLessThan__50
d_hasNonTrivialDivisor'45''8804'_698 :: Integer
-> Integer
-> Integer
-> T__HasNonTrivialDivisorLessThan__50
-> T__'8804'__22
-> T__HasNonTrivialDivisorLessThan__50
d_hasNonTrivialDivisor'45''8804'_698 ~Integer
v0 ~Integer
v1 ~Integer
v2 T__HasNonTrivialDivisorLessThan__50
v3 T__'8804'__22
v4
  = T__HasNonTrivialDivisorLessThan__50
-> T__'8804'__22 -> T__HasNonTrivialDivisorLessThan__50
du_hasNonTrivialDivisor'45''8804'_698 T__HasNonTrivialDivisorLessThan__50
v3 T__'8804'__22
v4
du_hasNonTrivialDivisor'45''8804'_698 ::
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__HasNonTrivialDivisorLessThan__50 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.Nat.Divisibility.Core.T__HasNonTrivialDivisorLessThan__50
du_hasNonTrivialDivisor'45''8804'_698 :: T__HasNonTrivialDivisorLessThan__50
-> T__'8804'__22 -> T__HasNonTrivialDivisorLessThan__50
du_hasNonTrivialDivisor'45''8804'_698 T__HasNonTrivialDivisorLessThan__50
v0 T__'8804'__22
v1
  = case T__HasNonTrivialDivisorLessThan__50
-> T__HasNonTrivialDivisorLessThan__50
forall a b. a -> b
coe T__HasNonTrivialDivisorLessThan__50
v0 of
      MAlonzo.Code.Data.Nat.Divisibility.Core.C_hasNonTrivialDivisor_72 Integer
v2 T__'8804'__22
v4 T__'8739'__20
v5
        -> (Integer
 -> T__'8804'__22
 -> T__'8739'__20
 -> T__HasNonTrivialDivisorLessThan__50)
-> Integer
-> Any
-> T__'8739'__20
-> T__HasNonTrivialDivisorLessThan__50
forall a b. a -> b
coe
             Integer
-> T__'8804'__22
-> T__'8739'__20
-> T__HasNonTrivialDivisorLessThan__50
MAlonzo.Code.Data.Nat.Divisibility.Core.C_hasNonTrivialDivisor_72
             Integer
v2
             ((T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
                T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45''8804''45'trans_2992
                (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v4) (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v1))
             T__'8739'__20
v5
      T__HasNonTrivialDivisorLessThan__50
_ -> T__HasNonTrivialDivisorLessThan__50
forall a. a
MAlonzo.RTE.mazUnreachableError