F64sqc.m10: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend as F64sqc
Lines 43-52 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend&start_line=43&end_line=52

import Base
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/natcmp.bend as NC

def m10(+m: Nat, +hl: {Nat.is_lt(m, 2n) == True{} : Bool}, +h: {Nat.is_eq(m, 0n) == False{} : Bool}) -> {m == 1n : Nat}:
  match m:
    case 0n:
      NC.absurd_tf({0n == 1n : Nat}, Equal.sym(Bool, True{}, False{}, h))
    case 1n+ +mp:
      match mp:
        case 0n:
          {==}
        case 1n+ +mq:
          Empty.absurd({2n+mq == 1n : Nat}, N.lt_zero_absurd(mq, hl))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_zero_absurd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend&name=absurd_tf