def wn.lt_add_r

bend-osdev-word64@0.1.1.0 · proof_value.bend:178

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

178def wn.lt_add_r(+x: Nat, +y: Nat, +a: Nat) -> {Nat.is_lt(Nat.add(x, a), Nat.add(y, a)) == Nat.is_lt(x, y) : Bool}:
179  %UL.nat_add_comm(a, x) : {Nat.is_lt(_, Nat.add(y, a)) == Nat.is_lt(x, y) : Bool}
180  %UL.nat_add_comm(a, y) : {Nat.is_lt(Nat.add(a, x), _) == Nat.is_lt(x, y) : Bool}
181  wn.lt_add_l(a, x, y)