def na.le_add

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1701

import Base

1701# b <= a + b
1702def na.le_add(+a: Nat, +b: Nat) -> {Nat.is_le(b, Nat.add(a, b)) == True{} : Bool}:
1703  match b:
1704    case 0n:
1705      %Equal.sym(Nat, Nat.add(a, 0n), a, na.add_zero(a)) : {Nat.is_le(0n, _) == True{} : Bool}
1706      na.le_zero(a)
1707    case 1n+p:
1708      %Equal.sym(Nat, Nat.add(a, 1n+p), 1n+Nat.add(a, p), na.add_succ(a, p)) : {Nat.is_le(1n+p, _) == True{} : Bool}
1709      na.le_add(a, p)