generalize Hcut.
apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
(* first goal (left open) *)
- intro. rewrite right H1.
+ intro. rewrite < H1.
clear Hcut.
(* second goal (closed) *)
goal 14.
generalize (refl_equal nat O).
apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
(* first goal (left open) *)
- intro. rewrite right H1.
+ intro. rewrite < H1.
(* second goal (closed) *)
goal 13.
simplify. intros.