~/jendhub

def wsd.mlc

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

import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
import Base

132def wsd.mlc(+x: Nat, +y: Nat, +c: Nat, +h: {Nat.is_lt(Nat.mul(x, c), Nat.mul(y, c)) == True{} : Bool}) -> {Nat.is_lt(x, y) == True{} : Bool}:
133  wsd.mlc.go(Nat.is_lt(x, y), x, y, c, {==}, h)

Uses (5)

Used by (1)