Idris2Doc : Data.Nat.BSExtra

Data.Nat.BSExtra

This contains additional proofs on natural number.

Reexports

import public Data.Array.Index

0 ltPlusRight : LT m n -> LT (k + m) (k + n): Totality: total
Visibility: export
0 ltePlusSuccRight : LTE (k + S m) n -> LTE (S (k + m)) n: Totality: total
Visibility: export
0 ltePlusRight : (o : Nat) -> LTE m n -> LTE (o + m) (o + n): Totality: total
Visibility: export
0 ltPlusSuccRight' : (k : Nat) -> LTE (k + S m) n -> LT m n: Totality: total
Visibility: export
0 plusMinus' : (m : Nat) -> (n : Nat) -> LTE m n -> minus n m + m = n: Totality: total
Visibility: export
0 lteAddLeft : (x : Nat) -> LTE m n -> LTE m (x + n): Totality: total
Visibility: export
0 lteAddRight : (x : Nat) -> LTE m n -> LTE m (n + x): Totality: total
Visibility: export
0 concatLemma1 : LTE (k + m) (k + (m + n)): Totality: total
Visibility: export
0 concatLemma2 : l + (k + m) = n -> (l + k) + m = n: Totality: total
Visibility: export
0 lteMinus : (n : Nat) -> LTE (S (minus n 0)) (S n): Totality: total
Visibility: export
0 minusLT : (m : Nat) -> (n : Nat) -> LT m n -> LT (minus n (S m)) n: Totality: total
Visibility: export