commit by user andrea

[helm.git] / weblib / arithmetics / bigops.ma

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