def sqmono

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqa.bend:28

import Base

28def sqmono(+a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.mul(a, a), Nat.mul(b, b)) == True{} : Bool}:
29  mle2(a, b, a, b, h, h)