law sa

lawful-fields@0.1.1.0 · proof_cut.bend:486

import Base

486law sa:
487  for +s: Nat
488  for +l: Nat
489  {Nat.sub(Nat.add(Nat.add(s, 1n), l), s) == 1n+l : Nat}