- by _ we proved (O = S (m1+n1*S m1)) (absurd_hyp').
- (* BUG: automation failure *)
- by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd).
- (* BUG: automation failure *)
- by (False_ind ? the_absurd)
- done.
+ we proved (O = S (m1+n1*S m1)) (absurd_hyp').
+ we proved False (the_absurd).
+ we proceed by cases on the_absurd to prove (S n1=O ∨ S m1=O).