def cnt1_le1

minebender-game@1.0.0.0 · proof_gen.bend:1013

import Base

1013def cnt1_le1(+a: Nat, +n: Nat) -> {Nat.is_le(cnt1(a, List.range(n)), 1n) == True{} : Bool}:
1014  match a:
1015    case 0n:
1016      %Equal.sym(Nat, cnt1(0n, List.range(n)), 0n, cnt1_zero(List.range(n))) : {Nat.is_le(_, 1n) == True{} : Bool}
1017      {==}
1018    case 1n+k:
1019      %Equal.sym(Nat, cnt1(1n+k, List.range(n)), cnt(k, List.range(n)), cnt1_succ(k, List.range(n))) :
1020        {Nat.is_le(_, 1n) == True{} : Bool}
1021      cnt_le1(k, n)