theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
intro.elim n.reflexivity.
apply False_ind.
-(* non si applica not_le_Sn_O *)
-apply (not_le_Sn_O ? H1).
+apply not_le_Sn_O.
+goal 17. apply H1.
qed.
theorem le_n_O_elim: \forall n:nat.n \leq O \to \forall P: nat \to Prop.