def halve_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqc.bend:54

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

54def halve_c(+x: Nat, +y: Nat, +h: {Nat.is_le(Nat.add(x, x), Nat.add(y, y)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_le(x, y) == c : Bool}) -> {c == True{} : Bool}:
55  match c:
56    case True{}:
57      {==}
58    case False{}:
59      +l = FL.add_lt2(y, x, N.not_le_lt(x, y, hc))
60      Equal.trans(Bool, False{}, Nat.is_le(Nat.add(x, x), Nat.add(y, y)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(x, x), Nat.add(y, y)), False{}, N.lt_not_le(Nat.add(y, y), Nat.add(x, x), l)), h)