Introduce `Mod a b < b` constraint

[sourabhxyz]

We would always have Mod a b to be less than (and by extension less than or equal to) b when b is not zero.

I tried:

instance (KnownNat a, KnownNat b, (1 <= b) ~ (() :: Constraint), m ~ Mod a b) => KnownBoolNat2 $(nameToSymbol ''(<=?)) m b where
  boolNatSing2 = SBoolKb (rem (natVal (Proxy @a)) (natVal (Proxy @b)) <= natVal (Proxy @b))
  {-# NOINLINE boolNatSing2 #-}

but that of course leads to duplicate instance.

[christiaanb]

I think this belongs in https://github.com/clash-lang/ghc-typelits-extra