~/jendhub

def aes_nat_succ_ne_zero

qasim-bend-kit@0.1.0.2 · PROOF.bend:387

import qasim-bend-kit@0.1.0.2/PROOF.bend as PROOF
import Base
import qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend as PrimitiveProof

387def aes_nat_succ_ne_zero(+p: Nat) -> {1n+p != 0n : Nat}:
388    e => PrimitiveProof.absurd(Empty,
389        PrimitiveProof.false_true(
390            Equal.cong(Nat, Bool, n => Nat.is_eq(n, 0n),
391                1n+p, 0n, e)))

Uses (7)

Used by (0)

No other definition uses this definition.