def pred_double

bend-collections-laws-math@1.0.0.0 · proofs/lib/nat.bend:467

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

467# pred(2v) == 1 + 2 pred(v) for v >= 1.
468def pred_double(+v: Nat, e: {Nat.is_le(1n, v) == True{} : Bool}) -> {Nat.sub(Nat.double(v), 1n) == 1n+Nat.double(Nat.sub(v, 1n)) : Nat}:
469  match v:
470    case 0n:
471      Empty.absurd({Nat.sub(0n, 1n) == 1n+Nat.double(Nat.sub(0n, 1n)) : Nat}, L.false_true(e))
472    case 1n+p:
473      %Equal.sym(Nat, Nat.sub(p, 0n), p, sub_zero(p)) : {1n+Nat.double(p) == 1n+Nat.double(_) : Nat}
474      {==}