def internal_nat_le_total_of_not_le

bend-mathlib@0.8.1.0 · order.bend:111

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

111def internal_nat_le_total_of_not_le(+a: Nat, +b: Nat, h: {Nat.is_le(a, b) == False{} : Bool}) -> MNat.le(b, a):
112  le_total_of_not_le(~Nat, ~Nat.is_le, ~internal_nat_le_total, a, b, h)