propagating the arithmetics library, partial commit

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / ynat_le.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le.ma
index 66a47dd4a0b4f6bd30a7dc0d40c18ed8dd29e859..1e1dad37f7f2bbe6f12c60f10ad40bbb0ca1e8ae 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le.ma
@@ -71,7 +71,8 @@ qed-.
 lemma yle_antisym (x) (y):
       x ≤ y → y ≤ x → x = y.
 #x #y #H elim H -x -y
-[ /4 width=1 by yle_inv_inj_bi, nle_antisym, eq_f/
+[ #m #n #Hmn #Hnm
+  <(nle_antisym … Hmn) -Hmn /2 width=1 by yle_inv_inj_bi/
 | /2 width=1 by yle_inv_inf_sn/
 ] 
 qed-.