law le_add

minebender-game@1.0.0.0 · proof_base.bend:707

import Base

707law le_add:
708  for +a: Nat
709  for +b: Nat
710  for +c: Nat
711  for +d: Nat
712  for e1: {Nat.is_le(a, b) == True{} : Bool}
713  for e2: {Nat.is_le(c, d) == True{} : Bool}
714  {Nat.is_le(Nat.add(a, c), Nat.add(b, d)) == True{} : Bool}