def ns.le_add_mono_r

bend-osdev-word64@0.1.1.0 · proof_shift.bend:182

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-word64@0.1.1.0/proof_value.bend as P

182def ns.le_add_mono_r(+a: Nat, +b: Nat, +c: Nat, h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}:
183  %UL.nat_add_comm(c, a) : {Nat.is_le(_, Nat.add(b, c)) == True{} : Bool}
184  %UL.nat_add_comm(c, b) : {Nat.is_le(Nat.add(c, a), _) == True{} : Bool}
185  Equal.trans(Bool, Nat.is_le(Nat.add(c, a), Nat.add(c, b)), Nat.is_le(a, b), True{}, P.wn.le_add_l(c, a, b), h)