def double_succ_le

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

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

433def double_succ_le(+n: Nat, e: {Nat.is_le(1n, n) == True{} : Bool}) -> {Nat.is_le(1n+n, Nat.double(n)) == True{} : Bool}:
434  match n:
435    case 0n:
436      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, L.false_true(e))
437    case 1n+p:
438      double_self_le(p)