law rsum_le

minebender-game@1.0.0.0 · proof_gen.bend:1097

import Base

1097law rsum_le:
1098  for +fy: Nat
1099  for +c: Nat
1100  for +ys: List<&2, Nat>
1101  for +lc: {Nat.is_le(c, 3n) == True{} : Bool}
1102  {Nat.is_le(rsum(fy, c, ys), Nat.add(Nat.add(ncnt(fy, ys), ncnt(fy, ys)), ncnt(fy, ys))) == True{} : Bool}