  let x = xp `mod` a in
  let y = yp `mod` b in
  Divides.chineseRemainder a b x y < a * b

proposition10 ::
  Primitive.Natural.Natural -> Primitive.Natural.Natural ->
    Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool