def two_le

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:684

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL

684def two_le(+k: Nat, +h1: {Nat.is_le(1n, k) == True{} : Bool}, +h2: {Nat.is_eq(k, 1n) == False{} : Bool}) -> {Nat.is_le(2n, k) == True{} : Bool}:
685  match k:
686    case 0n:
687      Empty.absurd({Nat.is_le(2n, 0n) == True{} : Bool}, FL.true_ne_false(Equal.sym(Bool, False{}, True{}, h1)))
688    case 1n:
689      Empty.absurd({Nat.is_le(2n, 1n) == True{} : Bool}, FL.true_ne_false(h2))
690    case 2n+ +kp:
691      N.zero_le(kp)