ProofGen.cnt1_le1: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
Lines 1013-1021 of minebender-game@1.0.0.0/proof_gen.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_gen.bend&start_line=1013&end_line=1021

import Base

def cnt1_le1(+a: Nat, +n: Nat) -> {Nat.is_le(cnt1(a, List.range(n)), 1n) == True{} : Bool}:
  match a:
    case 0n:
      %Equal.sym(Nat, cnt1(0n, List.range(n)), 0n, cnt1_zero(List.range(n))) : {Nat.is_le(_, 1n) == True{} : Bool}
      {==}
    case 1n+k:
      %Equal.sym(Nat, cnt1(1n+k, List.range(n)), cnt(k, List.range(n)), cnt1_succ(k, List.range(n))) :
        {Nat.is_le(_, 1n) == True{} : Bool}
      cnt_le1(k, n)

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.range
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=cnt
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=cnt1
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=cnt1_succ
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=cnt1_zero
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=cnt_le1