(no commit message)

[helm.git] / matita / library / nat / orders.ma

diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma
index 8c6ce942e33b0d272a8cadbbaabbc48e93eb6e49..3257e2e1a623d1f348f9d149bba0a0c7478355e2 100644 (file)
--- a/matita/library/nat/orders.ma
+++ b/matita/library/nat/orders.ma
@@ -182,8 +182,8 @@ qed.
 theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
 intro.elim n.reflexivity.
 apply False_ind.
-apply not_le_Sn_O.
-goal 17. apply H1.
+apply not_le_Sn_O;
+[2: apply H1 | skip].
 qed.
 
 theorem le_n_O_elim: \forall n:nat.n \leq O \to \forall P: nat \to Prop.
@@ -201,7 +201,7 @@ apply H2.reflexivity.
 apply H3. apply le_S_S. assumption.
 qed.
 
-(* le to eq *)
+(* le and eq *)
 lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
 apply nat_elim2
   [intros.apply le_n_O_to_eq.assumption