X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Farithmetics%2Fbigops.ma;fp=weblib%2Farithmetics%2Fbigops.ma;h=41c680088eb9987e563a0eac5985c4fb573048e0;hb=deff2f761d3e025908b6006c6fe3c07f1aa28d64;hp=0c10b02bb62200c21c222b3e364a400535317765;hpb=e81cff3104cd52f5a8d511b2802c42f7e1aa4d91;p=helm.git

diff --git a/weblib/arithmetics/bigops.ma b/weblib/arithmetics/bigops.ma
index 0c10b02bb..41c680088 100644
--- a/weblib/arithmetics/bigops.ma
+++ b/weblib/arithmetics/bigops.ma
@@ -322,7 +322,7 @@ qed.
 @(a href="cic:/matita/arithmetics/nat/le_gen.def(1)"le_gen/a ? n1) #i generalize in match p2; (elim i) 
   [(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
    >a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a 
-    [@(Hind ? (a href="cic:/matita/arithmetics/nat/le_O_n.def(2)"le_O_n/a ?)) [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/bigops/sub_hkO.def(4)"sub_hkO/a/span/span/ | @(a href="cic:/matita/arithmetics/bigops/transitive_sub.def(4)"transitive_sub/a … (a href="cic:/matita/arithmetics/bigops/sub_lt.def(5)"sub_lt/a …) sub2) //]
+    [@(Hind ? (a href="cic:/matita/arithmetics/nat/le_O_n.def(2)"le_O_n/a ?)) [@a href="cic:/matita/arithmetics/bigops/sub_hkO.def(4)"sub_hkO/a % | @(a href="cic:/matita/arithmetics/bigops/transitive_sub.def(4)"transitive_sub/a … (a href="cic:/matita/arithmetics/bigops/sub_lt.def(5)"sub_lt/a …) sub2) //]
     |@(a href="cic:/matita/arithmetics/bigops/sub0_to_false.def(4)"sub0_to_false/a … sub2) //
     ]
   |#n #Hind #p2 #ltn #sub1 #sub2 (cut (n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/an1)) [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/] #len