def pow2_mono

bend-collections-laws-math@1.0.0.0 · proofs/lib/nat.bend:450

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC

450# 1 <= n gives 1 + n <= 2n.
451def pow2_mono(+a: Nat, +b: Nat, e: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(SC.pow2(a), SC.pow2(b)) == True{} : Bool}:
452  match a b:
453    case 0n _:
454      pow2_pos(b)
455    case 1n+p 0n:
456      Empty.absurd({Nat.is_le(SC.pow2(1n+p), 1n) == True{} : Bool}, L.false_true(e))
457    case 1n+p 1n+q:
458      double_le(SC.pow2(p), SC.pow2(q), pow2_mono(p, q, e))