New axioms

[SkorikGG]

These might be useful for Data.Constraint.Nat

plusMonotone1' :: forall a b c. (a + c <= b + c):-(a <= b)
plusMonotone1' = Sub axiom

plusMonotone2' :: forall a b c. (a + b <= a + c):-(b <= c)
plusMonotone2' = Sub axiom

powMonotone1' :: forall a b c. ((a^c) <= (b^c),1<=c):-(a <= b)
powMonotone1' = Sub axiom

powMonotone2' :: forall a b c. ((a^b) <= (a^c),1<=a):-(b <= c)
powMonotone2' = Sub axiom

timesMonotone1' :: forall a b c. (a * c <= b * c,1<=c):-(a <= b)
timesMonotone1' = Sub axiom

timesMonotone2' :: forall a b c. (a * b <= a * c,1<=a):-(b <= c)
timesMonotone2' = Sub axiom

flipLT :: forall m n. (CmpNat m n ~ LT):-(CmpNat n m ~ GT)
flipLT = Sub axiom

flipGT :: forall m n. (CmpNat m n ~ GT):-(CmpNat n m ~ LT)
flipGT = Sub axiom

ltIsSuccLe :: forall m n. (CmpNat m n ~ LT):-(m+1<=n)
ltIsSuccLe = Sub $ axiomLe @(m+1) @n

succLeIsLT :: forall m n. (m+1<=n):-(CmpNat m n ~ LT)
succLeIsLT = Sub axiom 

ltIsLE :: forall m n. (CmpNat m n ~ LT):-(m<=n)
ltIsLE = Sub axiom -- Sub $ Dict \\ leTrans @m @(m+1) @n \\ ltIsSuccLe @m @n \\ plusMonotone2 @m @0 @1

gtIsNotLE :: forall m n. (CmpNat m n ~ GT):-((m <=? n) ~ False)
gtIsNotLE = Sub axiom

notLeIsGT :: forall m n. ((m <=? n) ~ False):-(CmpNat m n ~ GT)
notLeIsGT = Sub axiom

-- A more strict version
modBound' :: forall m n. (1 <= n) :- (CmpNat  (Mod m n)  n ~ LT)
modBound' = Sub axiom

Axioms for the minus operator:

minusNat :: forall n m. (KnownNat n, KnownNat m, m<=n) :- KnownNat (n - m)
minusNat = Sub $ case magic @n @m (-) of Sub r -> r

plusMinus :: forall m n. Dict (((m+n)-n) ~ m)
plusMinus = axiom

minusPlus :: forall n m. (n<=m):-(((m-n)+n) ~ m)
minusPlus = Sub axiom

minusIsCancellative1 :: forall m n o. ((m-n) ~ (o-n),n<=m):-(m~o)
minusIsCancellative1 = Sub axiom

minusIsCancellative2 :: forall m n o. ((m-n) ~ (m-o),n<=m):-(n~o)
minusIsCancellative2 = Sub axiom

minusMonotone1 :: forall a b c. (a <= b,c<=a):-(a - c <= b - c)
minusMonotone1 = Sub axiom

minusMonotone1' :: forall a b c. (a - c <= b - c,c<=a):-(a <= b)
minusMonotone1' = Sub axiom

minusMonotone2 :: forall a b c. (a <= b,b <= c):-(c - b <= c - a)
minusMonotone2 = Sub axiom

minusMonotone2' :: forall a b c. (c - b <= c - a,b<=c):-(a <= b)
minusMonotone2' = Sub axiom

[hellwolf]

Looks really useful, shall we just make a pull request?