def lt_dbl

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/final.bend:154

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend as A

154# x < 2x for x >= 1
155def lt_dbl(+x: Nat, +h: {Nat.is_le(1n, x) == True{} : Bool}) -> {Nat.is_lt(x, Nat.double(x)) == True{} : Bool}:
156  A.lt_subst(x, Nat.add(x, x), Nat.double(x), A.sy(Nat.double(x), Nat.add(x, x), NA.double_self(x)),
157    A.lt_substl(Nat.add(x, 0n), x, Nat.add(x, x), N.add_zero(x), N.lt_add_left(0n, x, x, N.succ_le_lt(0n, x, h))))