X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Farith_2b.ma;h=842fcc72a21f77e2fd3135f92e4047da878daa20;hp=f284a3c6cadc551ea4b29f44991426f1cd4becec;hb=6604a232815858a6c75dd25ac45abd68438077ff;hpb=888840f6b3a71d3d686b53b702d362ab90ab0038

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/arith_2b.ma b/matita/matita/contribs/lambdadelta/ground/arith/arith_2b.ma
index f284a3c6c..842fcc72a 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/arith_2b.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/arith_2b.ma
@@ -22,7 +22,8 @@ lemma arith_l4 (m11) (m12) (m21) (m22):
 elim (nat_split_le_ge (m11+m12) m21) #Hm1121
 [ lapply (nle_trans m11 ??? Hm1121) // #Hm121
   lapply (nle_minus_dx_dx … Hm1121) #Hm12211
-  <nminus_plus_comm_23 // @eq_f2 // <(nle_inv_eq_zero_minus m11 ?) // <(nle_inv_eq_zero_minus m12 ?) //
+  <nminus_plus_comm_23 // @eq_f2 //
+  <(nle_inv_eq_zero_minus m11 ?) // <(nle_inv_eq_zero_minus m12 ?) //
 | <(nle_inv_eq_zero_minus m21 ?) // <nplus_zero_sn <nminus_plus_assoc <nplus_comm
   elim (nat_split_le_ge m11 m21) #Hm121
   [ lapply (nle_minus_sn_dx … Hm1121) #Hm2112