PROOFText.wsd.mlc.go: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
Lines 125-130 of bend-osdev-word64@0.1.1.0/PROOF_text.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&start_line=125&end_line=130

import Base
import bend-osdev-word64@0.1.1.0/proof_value.bend as P
import bend-osdev-word64@0.1.1.0/proof_shift.bend as PS
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO

def wsd.mlc.go(b: Bool, +x: Nat, +y: Nat, +c: Nat, +eb: {Nat.is_lt(x, y) == b : Bool}, +h: {Nat.is_lt(Nat.mul(x, c), Nat.mul(y, c)) == True{} : Bool}) -> {Nat.is_lt(x, y) == True{} : Bool}:
  match b:
    case True{}:
      eb
    case False{}:
      Empty.absurd({Nat.is_lt(x, y) == True{} : Bool}, P.wn.lt_irrefl(Nat.mul(y, c), UO.nat_le_lt_trans(Nat.mul(y, c), Nat.mul(x, c), Nat.mul(y, c), wsd.mle(y, x, c, PS.ns.le_of_not_lt(x, y, eb)), h)))

Uses (9):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS_order.bend&name=nat_le_lt_trans
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsd.mle
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ns.le_of_not_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.lt_irrefl