def internal_lt_of_not_le

bend-mathlib@0.8.1.0 · nat.bend:2869

import bend-mathlib@0.8.1.0/nat.bend as Nat

import Base

2869def internal_lt_of_not_le(+a: Nat, +b: Nat, v: Bool, e: {v == Nat.is_lt(a, b) : Bool}, f: le(b, a) -> Empty) -> lt(a, b):
2870  match v:
2871    case True{}:
2872      Equal.sym(Bool, True{}, Nat.is_lt(a, b), e)
2873    case False{}:
2874      Empty.absurd(lt(a, b), f(le_of_not_lt(a, b, Equal.sym(Bool, False{}, Nat.is_lt(a, b), e))))

Uses (9)

Used by (2)