def d11_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64adds.bend:36

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

36def d11_c(+d: Nat, +S1: Nat, +c: Bool, +hc: {Nat.is_le(d, 10n) == c : Bool}, +hl: {Nat.is_eq(C.low(d, C.shift(10n, S1)), 0n) == False{} : Bool}) -> {Nat.is_le(11n, d) == True{} : Bool}:
37  match c:
38    case True{}:
39      Empty.absurd({Nat.is_le(11n, d) == True{} : Bool}, LW.true_ne_false(Equal.trans(Bool, True{}, Nat.is_eq(C.low(d, C.shift(10n, S1)), 0n), False{}, Equal.sym(Bool, Nat.is_eq(C.low(d, C.shift(10n, S1)), 0n), True{}, Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), C.low(d, C.shift(10n, S1)), 0n, low_sh(d, 10n, S1, hc))), hl)))
40    case False{}:
41      Equal.trans(Bool, Nat.is_le(11n, d), Nat.is_lt(10n, d), True{}, FR.le_succ_lt(10n, d), N.not_le_lt(d, 10n, hc))