def nat.gt_le_ne

bend-osdev-algo@0.1.0.0 · PROOF.bend:972

import Base

972# k < a (not a < k, a != k), a <= b: b != k
973def nat.gt_le_ne(a: Nat, b: Nat, k: Nat, e: {Nat.is_lt(a, k) == False{} : Bool}, f: {Nat.is_eq(a, k) == False{} : Bool}, g: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_eq(b, k) == False{} : Bool}:
974  match a b k:
975    case 0n _ 0n:
976      Empty.absurd({Nat.is_eq(b, 0n) == False{} : Bool}, absurd.tf(f))
977    case 0n _ 1n+kp:
978      Empty.absurd({Nat.is_eq(b, 1n+kp) == False{} : Bool}, absurd.tf(e))
979    case 1n+ap 0n _:
980      Empty.absurd({Nat.is_eq(0n, k) == False{} : Bool}, absurd.ft(g))
981    case 1n+ap 1n+bp 0n:
982      {==}
983    case 1n+ap 1n+bp 1n+kp:
984      nat.gt_le_ne(ap, bp, kp, e, f, g)