fact: Definition next_board n s gl v m b := let b1 := make_move n m b in if eq_board b b1 then iresult else if is_won v b1 then wresult else let z := zeros b1 in if z =? 0 then lresult else match add_val s gl b1 with | None => lresult | Some (s2, b2) => vresult s2 b2 end.
imports: Ascii String List EqNat NArith