law le_add

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/chacha/involution.bend:57

import Base

57law le_add:
58  for +p: Nat
59  for +l: Nat
60  for +k: Nat
61  for +h: {Nat.is_le(p, l) == True{} : Bool}
62  {Nat.is_le(p, Nat.add(k, l)) == True{} : Bool}