def pred_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addg.bend:92

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

92def pred_eq(+n: Nat, +hz: {Nat.is_eq(n, 0n) == False{} : Bool}) -> {1n+N.pred(n) == n : Nat}:
93  match n:
94    case 0n:
95      NC.absurd_tf({1n+N.pred(0n) == 0n : Nat}, Equal.sym(Bool, True{}, False{}, hz))
96    case 1n+ +np:
97      {==}