mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-10-26 12:08:29 +03:00
prove little lemma
This commit is contained in:
parent
82c9fdeb92
commit
ebb3436bbb
@ -2,5 +2,8 @@ Nat.lte.slack_right(
|
||||
a: Nat, b: Nat, c: Nat
|
||||
H: Equal(Bool, Nat.lte(a, b), true)
|
||||
): Equal(Bool, Nat.lte(a, Nat.add(b, c)), true)
|
||||
?Nat.lte.slack_right
|
||||
case Nat.add.comm(c, b) {
|
||||
refl:
|
||||
Nat.lte.slack_left(a, b, c, H)
|
||||
}: Equal(Bool, Nat.lte(a, self.b), true)
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user