def pick_lower

stelliferous@0.0.2.0 · proofs/nat_extrema.bend:68

import Base

68def pick_lower(choice: Bool,+left: Nat,+right: Nat,+lower: Nat,left_ok: {Nat.is_le(lower,left) == True{} : Bool},right_ok: {Nat.is_le(lower,right) == True{} : Bool}) ->
69  {Nat.is_le(lower,Bool.pick(Nat,choice,left,right)) == True{} : Bool}:
70  match choice:
71    case False{}: right_ok
72    case True{}: left_ok