def leb_mul

bend-ml-llama@0.2.1.0 · main.bend:550

import Base
import bend-ml-tensor-array@0.1.19.0/main.bend as TA

550# a <= b  ->  a·h <= b·h
551def leb_mul(a: Nat, b: Nat, +h: Nat, e: {True{} == TA.leb(a, b) : Bool}) -> {True{} == TA.leb(Nat.mul(a, h), Nat.mul(b, h)) : Bool}:
552  match a b:
553    case 0n _:
554      {==}
555    case 1n+p 0n:
556      %e : TA.BD(_, Unit, {True{} == TA.leb(Nat.mul(1n+p, h), 0n) : Bool})
557      Unit{}
558    case 1n++p 1n++q:
559      TA.leb_add(h, h, Nat.mul(p, h), Nat.mul(q, h), TA.leb_refl(h), leb_mul(p, q, h, e))