law le_add_r

lawful-words@0.1.0.0 · proof_nat.bend:779

import Base

779# a <= a + k and a <= k + a.
780law le_add_r:
781  for +a: Nat
782  for +k: Nat
783  {Nat.is_le(a, Nat.add(a, k)) == True{} : Bool}