have h2 : ¬ProblemPredicate 0 := by norm_num [ProblemPredicate]
case h.zero
h1 : ProblemPredicate 0
⊢ ProblemPredicate' (0 / 10) 0
case h.zero
h1 : ProblemPredicate 0
h2 : ¬ProblemPredicate 0
⊢ ProblemPredicate' (0 / 10) 0