def wsd.mlc.go

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:125

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

125def 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}:
126  match b:
127    case True{}:
128      eb
129    case False{}:
130      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)))