mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
Create add_left.kind
This commit is contained in:
parent
172fb18425
commit
6e8a09cc68
18
base/Nat/Order/add_left.kind
Normal file
18
base/Nat/Order/add_left.kind
Normal file
@ -0,0 +1,18 @@
|
||||
Nat.Order.add.left(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(a, b), true)
|
||||
): Equal<Bool>(Nat.lte(Nat.add(c, a), Nat.add(c, b)), true)
|
||||
(case c {
|
||||
zero:
|
||||
(Hyp)
|
||||
Hyp
|
||||
succ:
|
||||
(Hyp)
|
||||
Nat.Order.add.left(a, b, c.pred, Hyp)
|
||||
}:
|
||||
(Hyp: Equal<Bool>(Nat.lte(a, b), true)) ->
|
||||
Equal<Bool>(Nat.lte(Nat.add(c, a), Nat.add(c, b)), true))(
|
||||
Hyp
|
||||
)
|
Loading…
Reference in New Issue
Block a user