def ab_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64mont.bend:198

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
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/math/typed/natlight.bend as AQ

198def ab_lt(+bp: Nat, +a: Nat, +b: Nat, +ha: {Nat.is_lt(a, 1n+bp) == True{} : Bool}, +hb: {Nat.is_lt(b, 1n+bp) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(a, b), Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}:
199  N.le_lt_trans(Nat.mul(a, b), Nat.mul(a, 1n+bp), Nat.mul(1n+bp, 1n+bp), AQ.mle2(a, a, b, 1n+bp, N.le_refl(a), N.lt_le(b, 1n+bp, hb)), L.subst(Nat, z => {Nat.is_lt(Nat.mul(a, 1n+bp), z) == True{} : Bool}, Nat.mul(1n+bp, 1n+bp), Nat.mul(1n+bp, 1n+bp), {==}, lt_mul(a, 1n+bp, 1n+bp, ha, {==})))