def cnt_le1

minebender-game@1.0.0.0 · proof_gen.bend:1008

import minebender-game@1.0.0.0/proof_gen.bend as ProofGen

import Base

1008def cnt_le1(+i: Nat, +n: Nat) -> {Nat.is_le(cnt(i, List.range(n)), 1n) == True{} : Bool}:
1009  %Equal.sym(Nat, cnt(i, List.range(n)), Bool.pick(Nat, Nat.is_lt(i, n), 1n, 0n), cnt_range(i, n)) :
1010    {Nat.is_le(_, 1n) == True{} : Bool}
1011  pick_le1(Nat.is_lt(i, n))

Uses (10)

Used by (2)