def pow2_strict

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:460

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

460def pow2_strict(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(SC.pow2(a), SC.pow2(b)) == True{} : Bool}:
461  match b:
462    case 0n:
463      Empty.absurd({Nat.is_lt(SC.pow2(a), 1n) == True{} : Bool}, lt_zero_absurd(a, e))
464    case 1n+q:
465      lt_le_trans(SC.pow2(a), SC.pow2(1n+a), SC.pow2(1n+q), pow2_lt_succ(a), pow2_mono(1n+a, 1n+q, lt_succ_le_succ(a, 1n+q, e)))