def internal_div_not_succ_le
bend-mathlib@0.8.1.0 · nat.bend:909
import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base
909def internal_div_not_succ_le(a: Nat, bp: Nat, h: {False{} == Nat.is_le(1n+bp, a) : Bool}) -> {Nat.is_le(a, bp) == True{} : Bool}:
910 match a bp:
911 case 0n q:
912 Equal.sym(Bool, True{}, Nat.is_le(0n, q), internal_div_zero_le(q))
913 case 1n+ap 0n:
914 Empty.absurd({Nat.is_le(1n+ap, 0n) == True{} : Bool}, internal_div_true_ne_false(Equal.sym(Bool, False{}, True{}, Equal.trans(Bool, False{}, Nat.is_le(0n, ap), True{}, h, Equal.sym(Bool, True{}, Nat.is_le(0n, ap), internal_div_zero_le(ap))))))
915 case 1n+ap 1n+q:
916 internal_div_not_succ_le(ap, q, h)