def internal_le_flip_nat

bend-mathlib@0.8.1.0 · sort.bend:41

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

41def internal_le_flip_nat(x: Nat, y: Nat, e: {Nat.is_le(x, y) == False{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
42  match x y:
43    case 0n 0n:
44      Empty.absurd({True{} == True{} : Bool}, MNat.internal_false_ne_true(Equal.sym(Bool, True{}, False{}, e)))
45    case 0n 1n+q:
46      Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, MNat.internal_false_ne_true(Equal.sym(Bool, True{}, False{}, e)))
47    case 1n+p 0n:
48      {==}
49    case 1n+p 1n+q:
50      internal_le_flip_nat(p, q, e)