law reduce_inv
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/step.bend:274
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/step.bend as Step
import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend as Li
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as V
274law reduce_inv:
275 for +one: Nat
276 for +h1: {one == 1n : Nat}
277 for +d: List<&2, U32>
278 for +hd: {V.fit_all(d, 30n) == True{} : Bool}
279 {inv(Li.reduce(d)) == True{} : Bool}