X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fynat%2Fynat_le.ma;h=613a9793cb6a547b9e53ca49ce0307abaead7230;hb=2601d0c1a860fdd08c4c1d71473917aa85eeb63a;hp=b7b57d764ba64147c0a2acf3a34ab21497775f68;hpb=dd453d40e15929d6faef02f7b01a17f0cd6fc5b7;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma
index b7b57d764..613a9793c 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma
@@ -60,6 +60,11 @@ qed-.
 lemma yle_inv_Y1: ∀n. ∞ ≤ n → n = ∞.
 /2 width=3 by yle_inv_Y1_aux/ qed-.
 
+lemma yle_antisym: ∀y,x. x ≤ y → y ≤ x → x = y.
+#x #y #H elim H -x -y
+/4 width=1 by yle_inv_Y1, yle_inv_inj, le_to_le_to_eq, eq_f/
+qed-.
+
 (* Basic properties *********************************************************)
 
 lemma le_O1: ∀n:ynat. 0 ≤ n.