law le_add_mono_r

lawful-words@0.1.0.0 · proof_nat.bend:870

import Base

870law le_add_mono_r:
871  for +c: Nat
872  for +a: Nat
873  for +b: Nat
874  for h: {Nat.is_le(a, b) == True{} : Bool}
875  {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}