law Growth.add_left

gralha-bendquest@0.1.0.0 · growth.bend:21

import gralha-bendquest@0.1.0.0/growth.bend as Growth
import Base
import gralha-bendquest@0.1.0.0/game.bend as G

21law Growth.add_left:
22  for +a: Nat
23  for +b: Nat
24  for +extra: Nat
25  for +grow: {G.Bq.Nat.le(a, b) == True{} : Bool}
26  {G.Bq.Nat.le(G.Bq.Nat.add(a, extra), G.Bq.Nat.add(b, extra)) == True{} : Bool}

Uses (7)

Used by (1)