def mul_le_r

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:352

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR2

352def mul_le_r(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_le(Nat.mul(a, b), Nat.mul(a, c)) == True{} : Bool}:
353  +h1 = AR2.mul_le(b, c, a, h)
354  +h2 = L.subst(Nat, z => {Nat.is_le(z, Nat.mul(c, a)) == True{} : Bool}, Nat.mul(b, a), Nat.mul(a, b), NA.mul_comm(b, a), h1)
355  L.subst(Nat, z => {Nat.is_le(Nat.mul(a, b), z) == True{} : Bool}, Nat.mul(c, a), Nat.mul(a, c), NA.mul_comm(c, a), h2)