~/jendhub

def aes_nat_zero_ne_succ

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

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

381def aes_nat_zero_ne_succ(+p: Nat) -> {0n != 1n+p : Nat}:
382    e => PrimitiveProof.absurd(Empty,
383        PrimitiveProof.false_true(Equal.sym(Bool, True{}, False{},
384            Equal.cong(Nat, Bool, n => Nat.is_eq(n, 0n),
385                0n, 1n+p, e))))

Uses (8)

Used by (0)

No other definition uses this definition.