def not01

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/sel.bend:120

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg

120def not01(+c: Nat, +h: {Nat.is_lt(2n+c, 2n) == True{} : Bool}) -> Empty:
121  Lg.false_true(Equal.trans(Bool, False{}, Nat.is_lt(2n+c, 2n), True{}, Equal.sym(Bool, Nat.is_lt(2n+c, 2n), False{}, lt2(c)), h))