law Growth.add_both

gralha-bendquest@0.1.0.0 · growth.bend:53

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

53law Growth.add_both:
54  for +a: Nat
55  for +b: Nat
56  for +c: Nat
57  for +d: Nat
58  for +ab: {G.Bq.Nat.le(a, b) == True{} : Bool}
59  for +cd: {G.Bq.Nat.le(c, d) == True{} : Bool}
60  {G.Bq.Nat.le(G.Bq.Nat.add(a, c), G.Bq.Nat.add(b, d)) == True{} : Bool}