def dle_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:488

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

488def dle_c(+q: Nat, +p: Nat, +h: {Nat.is_le(Nat.double(q), Nat.double(p)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(p, q) == c : Bool}) -> {Nat.is_le(q, p) == True{} : Bool}:
489  match c:
490    case True{}:
491      Empty.absurd({Nat.is_le(q, p) == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(Nat.double(p), Nat.double(q)), False{}, Equal.sym(Bool, Nat.is_lt(Nat.double(p), Nat.double(q)), True{}, N.double_lt(p, q, hc)), N.le_not_lt(Nat.double(p), Nat.double(q), h))))
492    case False{}:
493      N.not_lt_le(p, q, hc)