def double_lt_inv

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/bgcdnat.bend:300

import Base

300# 2u < 2v gives u < v
301def double_lt_inv(+u: Nat, +v: Nat, +e: {Nat.is_lt(Nat.double(u), Nat.double(v)) == True{} : Bool}) -> {Nat.is_lt(u, v) == True{} : Bool}:
302  dlt_inv_b(u, v, e, Nat.is_lt(u, v), {==})