(.module:
  [library
   [lux #*
    ["_" test (#+ Test)]
    [abstract
     [monad (#+ do)]]
    [math
     ["." random (#+ Random)]
     [number
      ["." nat]
      ["." int]]]]]
  [\\library
   ["." /
    [//
     [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))))
            ))))