def pick_le3

minebender-game@1.0.0.0 · proof_gen.bend:1089

import Base

1089def pick_le3(+b: Bool, +c: Nat, lc: {Nat.is_le(c, 3n) == True{} : Bool}) ->
1090  {Nat.is_le(Bool.pick(Nat, b, c, 0n), Nat.add(Nat.add(one(b), one(b)), one(b))) == True{} : Bool}:
1091  match b:
1092    case True{}:
1093      lc
1094    case False{}:
1095      {==}