mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
Create add_right.kind
This commit is contained in:
parent
6e8a09cc68
commit
1a2ef75255
16
base/Nat/Order/add_right.kind
Normal file
16
base/Nat/Order/add_right.kind
Normal file
@ -0,0 +1,16 @@
|
||||
Nat.Order.add.right(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(a, b), true)
|
||||
): Equal<Bool>(Nat.lte(Nat.add(a, c), Nat.add(b, c)), true)
|
||||
let lem = Nat.Order.add.left(a, b, c, Hyp)
|
||||
let lem = Equal.rewrite<Nat>(
|
||||
Nat.add(c, a), Nat.add(a, c), Nat.add.comm(c, a),
|
||||
(x) Equal<Bool>(Nat.lte(x, Nat.add(c, b)), true), lem
|
||||
)
|
||||
let qed = Equal.rewrite<Nat>(
|
||||
Nat.add(c, b), Nat.add(b, c), Nat.add.comm(c, b),
|
||||
(x) Equal<Bool>(Nat.lte(Nat.add(a, c), x), true), lem
|
||||
)
|
||||
qed
|
Loading…
Reference in New Issue
Block a user