law add_le

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/value.bend:87

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend as Li

87law add_le:
88  for +a: List<&2, U32>
89  for +b: List<&2, U32>
90  for +b1: Nat
91  for +b2: Nat
92  for +ha: {le_all(a, b1) == True{} : Bool}
93  for +hb: {le_all(b, b2) == True{} : Bool}
94  for +hf: {C.fits(32n, Nat.add(b1, b2)) == True{} : Bool}
95  {le_all(Li.add(a, b), Nat.add(b1, b2)) == True{} : Bool}