def successor_pick

stelliferous@0.0.2.0 · proofs/nat_extrema.bend:7

import Base

7def successor_pick(choice: Bool,+left: Nat,+right: Nat) ->
8  {1n+Bool.pick(Nat,choice,left,right) == Bool.pick(Nat,choice,1n+left,1n+right) : Nat}:
9  match choice:
10    case False{}: {==}
11    case True{}: {==}