law rsum_at_full

minebender-game@1.0.0.0 · proof_sums.bend:199

import Base

199law rsum_at_full:
200  for ~A: Data
201  for ~f: A -> Nat
202  for +d: A
203  for +r: List<&2, A>
204  {rsum_at(~A, ~f, d, r, List.range(List.length(&2, A, r))) == rsum(~A, ~f, r) : Nat}