(.module:
  [library
   [lux "*"
    ["_" test {"+" [Test]}]
    [abstract
     [monad {"+" [do]}]]
    [math
     ["[0]" random {"+" [Random]}]
     [number
      ["[0]" nat]
      ["[0]" int]]]]]
  [\\library
   ["[0]" /
    [//
     [equivalence {"+" [Equivalence]}]]]])

(def: .public test
  Test
  (do random.monad
    [natL random.nat
     natR random.nat
     intL random.int
     intR random.int]
    (<| (_.covering /._)
        ($_ _.and
            (_.cover [/.and]
                     (let [[natLR intLR] (\ (/.and nat.addition int.multiplication) composite
                                            [natL intL] [natR intR])]
                       (and (nat.= (\ nat.addition composite natL natR)
                                   natLR)
                            (int.= (\ int.multiplication composite intL intR)
                                   intLR))))
            ))))