law sub_zero
import lawful-arrays@0.1.0.0/proof_base.bend as ProofBaseimport Base
125law sub_zero:
126 for +i: Nat
127 {Nat.sub(i, 0n) == i : Nat}
import lawful-arrays@0.1.0.0/proof_base.bend as ProofBaseimport Base
125law sub_zero:
126 for +i: Nat
127 {Nat.sub(i, 0n) == i : Nat}