def lt_add1

bend-collections-laws-math@1.0.0.0 · proofs/math/number/prime.bend:139

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A

139# e < e + (1 + p)
140def lt_add1(+e: Nat, +p: Nat) -> {Nat.is_lt(e, Nat.add(e, 1n+p)) == True{} : Bool}:
141  %Equal.sym(Nat, Nat.add(e, 1n+p), 1n+Nat.add(e, p), A.add_succ(e, p)) : {Nat.is_lt(e, _) == True{} : Bool}
142  N.le_lt_succ(e, Nat.add(e, p), N.le_add_right(e, p))