def un.lt_add_r

bend-osdev-u32@0.1.0.0 · PROOF.bend:235

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF

import Base

235def un.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}:
236  %un.add_comm(a, x) : {Nat.is_lt(_, Nat.add(y, a)) == Nat.is_lt(x, y) : Bool}
237  %un.add_comm(a, y) : {Nat.is_lt(Nat.add(a, x), _) == Nat.is_lt(x, y) : Bool}
238  un.lt_add_l(a, x, y)

Uses (6)

Used by (2)