X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Farithmetics%2Fbigops.ma;h=7936b5dd038455bea4104679104814fd7ce4d027;hb=79b20b5845577c9359b9a4218f8eedd2a322e416;hp=41c680088eb9987e563a0eac5985c4fb573048e0;hpb=ea368a02a071bb99eeb84bf24ab4000acb314d60;p=helm.git

diff --git a/weblib/arithmetics/bigops.ma b/weblib/arithmetics/bigops.ma
index 41c680088..7936b5dd0 100644
--- a/weblib/arithmetics/bigops.ma
+++ b/weblib/arithmetics/bigops.ma
@@ -42,25 +42,25 @@ qed.
       |false ⇒ bigop k p B nil op f]
    ].
    
-notation "\big  [ op , nil ]_{ ident i < n | p } f"
+notation "ref 'bigop \big  [ op , nil ]_{ ident i < n | p } f"
   with precedence 80
 for @{'bigop $n $op $nil (λ${ident i}. $p) (λ${ident i}. $f)}.
 
-notation "\big [ op , nil ]_{ ident i < n } f"
+notation "ref 'bigop \big [ op , nil ]_{ ident i < n } f"
   with precedence 80
 for @{'bigop $n $op $nil (λ${ident i}.true) (λ${ident i}. $f)}.
 
 interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
 
-notation "\big  [ op , nil ]_{ ident j ∈ [a,b[ | p } f"
+notation "ref 'bigop \big  [ op , nil ]_{ ident j ∈ [a,b[ | p } f"
   with precedence 80
-for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
-  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
+for @{'bigop (minus $b $a) $op $nil (λ${ident j}.((λ${ident j}.$p) (plus ${ident j} $a)))
+  (λ${ident j}.((λ${ident j}.$f)(plus ${ident j} $a)))}.
 
-notation "\big  [ op , nil ]_{ ident j ∈ [a,b[ } f"
+notation "ref 'bigop \big  [ op , nil ]_{ ident j ∈ [a,b[ } f"
   with precedence 80
-for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
-  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.  
+for @{'bigop (minus $b $a) $op $nil (λ${ident j}.((λ${ident j}.true) (plus ${ident j} $a)))
+  (λ${ident j}.((λ${ident j}.$f)(plus ${ident j} $a)))}.  
 
 (* notation "\big  [ op , nil ]_{( term 50) a ≤ ident j < b | p } f"
   with precedence 80
@@ -70,19 +70,19 @@ for @{\big[$op,$nil]_{${ident j} < ($b-$a) | ((λ${ident j}.$p) (${ident j}+$a))
 interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
    
 img class="anchor" src="icons/tick.png" id="bigop_Strue"lemma bigop_Strue: ∀k,p,B,nil,op.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. p k a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a →
-  \big[op,nil]_{i < a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
-    op (f k) (\big[op,nil]_{i < k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i)).
+  a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+    op (f k) (a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i)).
 #k #p #B #nil #op #f #H normalize >H // qed.
 
 img class="anchor" src="icons/tick.png" id="bigop_Sfalse"lemma bigop_Sfalse: ∀k,p,B,nil,op.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. p k a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a →
-  \big[op,nil]_{ i < a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
-    \big[op,nil]_{i < k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i).
+  a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{ i < a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+    a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i).
 #k #p #B #nil #op #f #H normalize >H // qed. 
  
 img class="anchor" src="icons/tick.png" id="same_bigop"lemma same_bigop : ∀k,p1,p2,B,nil,op.∀f,g:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. 
   a href="cic:/matita/arithmetics/bigops/sameF_upto.def(2)"sameF_upto/a k a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a p1 p2 → a href="cic:/matita/arithmetics/bigops/sameF_p.def(2)"sameF_p/a k p1 B f g →
-  \big[op,nil]_{i < k | p1 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-    \big[op,nil]_{i < k | p2 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(g i).
+  a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < k | p1 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+    a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < k | p2 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(g i).
 #k #p1 #p2 #B #nil #op #f #g (elim k) // 
 #n #Hind #samep #samef normalize >Hind 
   [|@(a href="cic:/matita/arithmetics/bigops/sameF_p_le.def(5)"sameF_p_le/a … samef) // |@(a href="cic:/matita/arithmetics/bigops/sameF_upto_le.def(5)"sameF_upto_le/a … samep) //]
@@ -91,8 +91,8 @@ normalize // <(samef … (a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le
 qed.
 
 img class="anchor" src="icons/tick.png" id="pad_bigop"theorem pad_bigop: ∀k,n,p,B,nil,op.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a k → 
-\big[op,nil]_{i < n | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i)
-  a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a \big[op,nil]_{i < k | font class="Apple-style-span" color="#FF0000"if/font (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n i) then a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a else p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i).
+a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < n | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i)
+  a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < k | font class="Apple-style-span" color="#FF0000"if/font (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n i) then a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a else p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i).
 #k #n #p #B #nil #op #f #lenk (elim lenk) 
   [@a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a #i #lti // >(a href="cic:/matita/arithmetics/nat/not_le_to_leb_false.def(7)"not_le_to_leb_false/a …) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a/span/span/
   |#j #leup #Hind >a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a >(a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"le_to_leb_true/a … leup) // 
@@ -100,8 +100,8 @@ qed.
 
 img class="anchor" src="icons/tick.png" id="pad_bigop1"theorem pad_bigop1: ∀k,n,p,B,nil,op.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a k → 
   (∀i. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a k → p i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) →
-  \big[op,nil]_{i < n | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) 
-    a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a \big[op,nil]_{i < k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i).
+  a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < n | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) 
+    a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i).
 #k #n #p #B #nil #op #f #lenk (elim lenk) 
   [#_ @a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a #i #lti // 
   |#j #leup #Hind #Hfalse >a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a 
@@ -112,7 +112,7 @@ qed.
 qed.
 
 img class="anchor" src="icons/tick.png" id="bigop_false"theorem bigop_false: ∀n,B,nil,op.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B.
-  \big[op,nil]_{i < n | a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a nil.  
+  a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < n | a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a nil.  
 #n #B #nil #op #f elim n // #n1 #Hind 
 >a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a // 
 qed.
@@ -126,8 +126,8 @@ qed.
 
 img class="anchor" src="icons/tick.png" id="pad_bigop_nil"theorem pad_bigop_nil: ∀k,n,p,B,nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a k → 
   (∀i. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a k → p i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="logical or" href="cic:/fakeuri.def(1)"∨/a f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a nil) →
-  \big[op,nil]_{i < n | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) 
-    a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a \big[op,nil]_{i < k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i).
+  a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < n | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) 
+    a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i).
 #k #n #p #B #nil #op #f #lenk (elim lenk) 
   [#_ @a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a #i #lti // 
   |#j #leup #Hind #Hfalse cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p j)) #Hpj
@@ -143,8 +143,8 @@ qed.
 qed.
 
 img class="anchor" src="icons/tick.png" id="bigop_sum"theorem bigop_sum: ∀k1,k2,p1,p2,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f,g:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B.
-op (\big[op,nil]_{i<k1|p1 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i)) \big[op,nil]_{i<k2|p2 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(g i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
-      \big[op,nil]_{i<k1a title="natural plus" href="cic:/fakeuri.def(1)"+/ak2|font class="Apple-style-span" color="#FF0000" if /fonta href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a k2 i then p1 (ia title="natural minus" href="cic:/fakeuri.def(1)"-/ak2) else p2 ia title="bigop" href="cic:/fakeuri.def(1)"}/a
+op (a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i<k1|p1 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i)) a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i<k2|p2 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(g i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+      a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i<k1a title="natural plus" href="cic:/fakeuri.def(1)"+/ak2|font class="Apple-style-span" color="#FF0000" if /fonta href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a k2 i then p1 (ia title="natural minus" href="cic:/fakeuri.def(1)"-/ak2) else p2 ia title="bigop" href="cic:/fakeuri.def(1)"}/a
         (if a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a k2 i then f (ia title="natural minus" href="cic:/fakeuri.def(1)"-/ak2) else g i).
 #k1 #k2 #p1 #p2 #B #nil #op #f #g (elim k1)
   [normalize >a href="cic:/matita/arithmetics/bigops/nill.fix(0,2,2)"nill/a @a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a #i #lti 
@@ -161,12 +161,12 @@ qed.
 qed.
 
 img class="anchor" src="icons/tick.png" id="bigop_I"theorem bigop_I: ∀n,p,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B.
-\big[op,nil]_{i∈[a title="natural number" href="cic:/fakeuri.def(1)"0/a,n[ |p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a \big[op,nil]_{i < n|p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i). 
+a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i∈[a title="natural number" href="cic:/fakeuri.def(1)"0/a,n[ |p ia title="natural minus" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < n|p i}(f i). 
 #n #p #B #nil #op #f <a href="cic:/matita/arithmetics/nat/minus_n_O.def(3)"minus_n_O/a @a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a //
 qed.
 
 img class="anchor" src="icons/tick.png" id="bigop_I_gen"theorem bigop_I_gen: ∀a,b,p,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/ab →
-\big[op,nil]_{i∈[a,b[ |p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a \big[op,nil]_{i < b|a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a a i a title="boolean and" href="cic:/fakeuri.def(1)"∧/a p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i). 
+a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i∈[a,b[ |p i}(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < b|a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a a i a title="boolean and" href="cic:/fakeuri.def(1)"∧/a p i}(f i). 
 #a #b elim b // -b #b #Hind #p #B #nil #op #f #lea
 cut (∀a,b. a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (b a title="natural minus" href="cic:/fakeuri.def(1)"-/aa)) 
   [#a #b cases a // #a1 #lta1 normalize >a href="cic:/matita/arithmetics/nat/eq_minus_S_pred.def(4)"eq_minus_S_pred/a >a href="cic:/matita/arithmetics/nat/S_pred.def(3)"S_pred/a 
@@ -193,9 +193,9 @@ qed.
           
 img class="anchor" src="icons/tick.png" id="bigop_sumI"theorem bigop_sumI: ∀a,b,c,p,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B.
 a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b → b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a c →
-\big[op,nil]_{i∈[a,c[ |p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-  op (\big[op,nil]_{i ∈ [b,c[ |p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i)) 
-      \big[op,nil]_{i ∈ [a,b[ |p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i).
+a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i∈[a,c[ |p i}(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+  op (a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i ∈ [b,c[ |p i}(f i)) 
+      a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i ∈ [a,b[ |p i}(f i).
 #a #b # c #p #B #nil #op #f #leab #lebc 
 >(a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a (ca title="natural minus" href="cic:/fakeuri.def(1)"-/aa) (ba title="natural minus" href="cic:/fakeuri.def(1)"-/aa)) in ⊢ (??%?); /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(9)"monotonic_le_minus_l/a/span/span/
 >a href="cic:/matita/arithmetics/nat/minus_plus.def(13)"minus_plus/a >(a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"commutative_plus/a a) <a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a //
@@ -206,24 +206,24 @@ a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b →
 qed.   
 
 img class="anchor" src="icons/tick.png" id="bigop_a"theorem bigop_a: ∀a,b,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b →
-\big[op,nil]_{i∈[a,a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a b[ a title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-  op (\big[op,nil]_{i ∈ [a,b[ a title="bigop" href="cic:/fakeuri.def(1)"}/a(f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i))) (f a).
+a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i∈[a,a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a b[ }(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+  op (a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i ∈ [a,b[ }(f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i))) (f a).
 #a #b #B #nil #op #f #leab 
 >(a href="cic:/matita/arithmetics/bigops/bigop_sumI.def(14)"bigop_sumI/a a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a a) (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a b)) [|@a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a //|//] @a href="cic:/matita/basics/logic/eq_f2.def(3)"eq_f2/a 
   [@a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a // |<a href="cic:/matita/arithmetics/nat/minus_Sn_n.def(4)"minus_Sn_n/a normalize @a href="cic:/matita/arithmetics/bigops/nilr.fix(0,2,2)"nilr/a]
 qed.
   
 img class="anchor" src="icons/tick.png" id="bigop_0"theorem bigop_0: ∀n,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B.
-\big[op,nil]_{i < a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a na title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-  op (\big[op,nil]_{i < na title="bigop" href="cic:/fakeuri.def(1)"}/a(f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i))) (f a title="natural number" href="cic:/fakeuri.def(1)"0/a).
+a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n}(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+  op (a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i < n}(f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i))) (f a title="natural number" href="cic:/fakeuri.def(1)"0/a).
 #n #B #nil #op #f 
 <a href="cic:/matita/arithmetics/bigops/bigop_I.def(7)"bigop_I/a >a href="cic:/matita/arithmetics/bigops/bigop_a.def(15)"bigop_a/a [|//] @a href="cic:/matita/basics/logic/eq_f2.def(3)"eq_f2/a [|//] <a href="cic:/matita/arithmetics/nat/minus_n_O.def(3)"minus_n_O/a 
 @a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a //
 qed.    
 
 img class="anchor" src="icons/tick.png" id="bigop_prod"theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a →a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → B.
-\big[op,nil]_{x<k1|p1 xa title="bigop" href="cic:/fakeuri.def(1)"}/a(\big[op,nil]_{i<k2|p2 x ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f x i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
-  \big[op,nil]_{i<k1a title="natural times" href="cic:/fakeuri.def(1)"*/ak2|a href="cic:/matita/basics/bool/andb.def(1)"andb/a (p1 (a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a i k2)) (p2 (a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a i k2) (i a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a k2))a title="bigop" href="cic:/fakeuri.def(1)"}/a
+a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{x<k1|p1 x}(a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i<k2|p2 x i}(f x i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+  a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i<k1a title="natural times" href="cic:/fakeuri.def(1)"*/ak2|a href="cic:/matita/basics/bool/andb.def(1)"andb/a (p1 (a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a i k2)) (p2 (a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a i k2) (i a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a k2))}
      (f (a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a i k2) (i a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a k2)).
 #k1 #k2 #p1 #p2 #B #nil #op #f (elim k1) //
 #n #Hind cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p1 n)) #Hp1
@@ -243,8 +243,8 @@ qed.
   }.
  
 img class="anchor" src="icons/tick.png" id="bigop_op"lemma bigop_op: ∀k,p,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"ACop/a B nil.∀f,g: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → B.
-op (\big[op,nil]_{i<k|p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i)) (\big[op,nil]_{i<k|p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(g i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
-  \big[op,nil]_{i<k|p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(op (f i) (g i)).
+op (a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i<k|p i}(f i)) (a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i<k|p i}(g i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+  a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i<k|p i}(op (f i) (g i)).
 #k #p #B #nil #op #f #g (elim k) [normalize @a href="cic:/matita/arithmetics/bigops/nill.fix(0,2,2)"nill/a]
 -k #k #Hind (cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p k))) #H
   [>a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a // >a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a // >a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a //
@@ -256,8 +256,8 @@ qed.
 
 img class="anchor" src="icons/tick.png" id="bigop_diff"lemma bigop_diff: ∀p,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"ACop/a B nil.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → B.∀i,n.
   i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → p i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a →
-  \big[op,nil]_{x<n|p xa title="bigop" href="cic:/fakeuri.def(1)"}/a(f x)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
-    op (f i) (\big[op,nil]_{x<n|a href="cic:/matita/basics/bool/andb.def(1)"andb/a(a href="cic:/matita/basics/bool/notb.def(1)"notb/a(a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a i x))(p x)a title="bigop" href="cic:/fakeuri.def(1)"}/a(f x)).
+  a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{x<n|p x}(f x)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+    op (f i) (a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{x<n|a href="cic:/matita/basics/bool/andb.def(1)"andb/a(a href="cic:/matita/basics/bool/notb.def(1)"notb/a(a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a i x))(p x)}(f x)).
 #p #B #nil #op #f #i #n (elim n) 
   [#ltO @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
   |#n #Hind #lein #pi cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … (a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a …lein)) #Hi
@@ -317,7 +317,7 @@ qed.
 
 img class="anchor" src="icons/tick.png" id="bigop_iso"theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"ACop/a B nil.∀f1,f2.
   a href="cic:/matita/arithmetics/bigops/iso.def(3)"iso/a B (a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"mk_range/a B f1 n1 p1) (a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"mk_range/a B f2 n2 p2) →
-  \big[op,nil]_{i<n1|p1 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f1 i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a \big[op,nil]_{i<n2|p2 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f2 i).
+  a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i<n1|p1 i}(f1 i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i<n2|p2 i}(f2 i).
 #n1 #n2 #p1 #p2 #B #nil #op #f1 #f2 * #h * #k * * #same
 @(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
@@ -353,8 +353,8 @@ qed.
 img class="anchor" src="icons/tick.png" id="bigop_commute"theorem bigop_commute: ∀n,m,p11,p12,p21,p22,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"ACop/a B nil.∀f.
 a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m →
 (∀i,j. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → j a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → (p11 i a title="boolean and" href="cic:/fakeuri.def(1)"∧/a p12 i j) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (p21 j a title="boolean and" href="cic:/fakeuri.def(1)"∧/a p22 i j)) →
-\big[op,nil]_{i<n|p11 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(\big[op,nil]_{j<m|p12 i ja title="bigop" href="cic:/fakeuri.def(1)"}/a(f i j)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
-   \big[op,nil]_{j<m|p21 ja title="bigop" href="cic:/fakeuri.def(1)"}/a(\big[op,nil]_{i<n|p22 i ja title="bigop" href="cic:/fakeuri.def(1)"}/a(f i j)).
+a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i<n|p11 i}(a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{j<m|p12 i j}(f i j)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+   a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{j<m|p21 j}(a title="bigop" href="cic:/fakeuri.def(1)"\big/a[op,nil]_{i<n|p22 i j}(f i j)).
 #n #m #p11 #p12 #p21 #p22 #B #nil #op #f #posn #posm #Heq
 >a href="cic:/matita/arithmetics/bigops/bigop_prod.def(15)"bigop_prod/a >a href="cic:/matita/arithmetics/bigops/bigop_prod.def(15)"bigop_prod/a @a href="cic:/matita/arithmetics/bigops/bigop_iso.def(9)"bigop_iso/a 
 %{(λi.(ia title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m)a title="natural times" href="cic:/fakeuri.def(1)"*/an a title="natural plus" href="cic:/fakeuri.def(1)"+/a ia title="natural divide" href="cic:/fakeuri.def(1)"//am)} %{(λi.(ia title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a n)a title="natural times" href="cic:/fakeuri.def(1)"*/am a title="natural plus" href="cic:/fakeuri.def(1)"+/a ia title="natural divide" href="cic:/fakeuri.def(1)"//an)} % 
@@ -407,8 +407,8 @@ qed.
 img class="anchor" src="icons/tick.png" id="bigop_distr"theorem bigop_distr: ∀n,p,B,nil.∀R:a href="cic:/matita/arithmetics/bigops/Dop.ind(1,0,2)"Dop/a B nil.\forall f,a.
   let aop \def  a href="cic:/matita/arithmetics/bigops/sum.fix(0,2,4)"sum/a B nil R in
   let mop \def a href="cic:/matita/arithmetics/bigops/prod.fix(0,2,4)"prod/a B nil R in
-  mop a \big[aop,nil]_{i<n|p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-   \big[aop,nil]_{i<n|p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(mop a (f i)).
+  mop a a title="bigop" href="cic:/fakeuri.def(1)"\big/a[aop,nil]_{i<n|p i}(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+   a title="bigop" href="cic:/fakeuri.def(1)"\big/a[aop,nil]_{i<n|p i}(mop a (f i)).
 #n #p #B #nil #R #f #a normalize (elim n) [@a href="cic:/matita/arithmetics/bigops/null.fix(0,2,5)"null/a]
 #n #Hind (cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p n))) #H
   [>a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a // >a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a // >(a href="cic:/matita/arithmetics/bigops/distr.fix(0,2,5)"distr/a B nil R) >Hind //