weblib/arithmetics/bigops.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "basics/types.ma".
  13 include "arithmetics/div_and_mod.ma".
  14
  15 \ 5img class="anchor" src="icons/tick.png" id="sameF_upto"\ 6definition sameF_upto: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → ∀A.\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→A)  ≝
  16 λk.λA.λf,g.∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 k → f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g i.
  17
  18 \ 5img class="anchor" src="icons/tick.png" id="sameF_p"\ 6definition sameF_p: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → (\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) →∀A.\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→A)  ≝
  19 λk,p,A,f,g.∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 k → p i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g i.
  20
  21 \ 5img class="anchor" src="icons/tick.png" id="sameF_upto_le"\ 6lemma sameF_upto_le: ∀A,f,g,n,m.
  22  n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6m → \ 5a href="cic:/matita/arithmetics/bigops/sameF_upto.def(2)"\ 6sameF_upto\ 5/a\ 6 m A f g → \ 5a href="cic:/matita/arithmetics/bigops/sameF_upto.def(2)"\ 6sameF_upto\ 5/a\ 6 n A f g.
  23 #A #f #g #n #m #lenm #samef #i #ltin @samef /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  24 qed.
  25
  26 \ 5img class="anchor" src="icons/tick.png" id="sameF_p_le"\ 6lemma sameF_p_le: ∀A,p,f,g,n,m.
  27  n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6m → \ 5a href="cic:/matita/arithmetics/bigops/sameF_p.def(2)"\ 6sameF_p\ 5/a\ 6 m p A f g → \ 5a href="cic:/matita/arithmetics/bigops/sameF_p.def(2)"\ 6sameF_p\ 5/a\ 6 n p A f g.
  28 #A #p #f #g #n #m #lenm #samef #i #ltin #pi @samef /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  29 qed.
  30
  31 \ 5img class="anchor" src="icons/tick.png" id="prodF"\ 6definition prodF ≝
  32  λA,B.λf:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→A.λg:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.λm,x.〈 f(\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 x m), g(\ 5a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"\ 6mod\ 5/a\ 6 x m) \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6.
  33
  34 (* bigop *)
  35 \ 5img class="anchor" src="icons/tick.png" id="bigop"\ 6let rec bigop (n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (B:Type[0])
  36    (nil: B) (op: B → B → B)  (f: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → B) ≝
  37   match n with
  38    [ O ⇒ nil
  39    | S k ⇒
  40       match p k with
  41       [true ⇒ op (f k) (bigop k p B nil op f)
  42       |false ⇒ bigop k p B nil op f]
  43    ].
  44
  45 notation "ref 'bigop \big  [ op , nil ]_{ ident i < n | p } f"
  46   with precedence 80
  47 for @{'bigop $n $op $nil (λ${ident i}. $p) (λ${ident i}. $f)}.
  48
  49 notation "ref 'bigop \big [ op , nil ]_{ ident i < n } f"
  50   with precedence 80
  51 for @{'bigop $n $op $nil (λ${ident i}.true) (λ${ident i}. $f)}.
  52
  53 interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
  54
  55 notation "ref 'bigop \big  [ op , nil ]_{ ident j ∈ [a,b[ | p } f"
  56   with precedence 80
  57 for @{'bigop (minus $b $a) $op $nil (λ${ident j}.((λ${ident j}.$p) (plus ${ident j} $a)))
  58   (λ${ident j}.((λ${ident j}.$f)(plus ${ident j} $a)))}.
  59
  60 notation "ref 'bigop \big  [ op , nil ]_{ ident j ∈ [a,b[ } f"
  61   with precedence 80
  62 for @{'bigop (minus $b $a) $op $nil (λ${ident j}.((λ${ident j}.true) (plus ${ident j} $a)))
  63   (λ${ident j}.((λ${ident j}.$f)(plus ${ident j} $a)))}.
  64
  65 (* notation "\big  [ op , nil ]_{( term 50) a ≤ ident j < b | p } f"
  66   with precedence 80
  67 for @{\big[$op,$nil]_{${ident j} < ($b-$a) | ((λ${ident j}.$p) (${ident j}+$a))}((λ${ident j}.$f)(${ident j}+$a))}.
  68 *)
  69
  70 interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
  71
  72 \ 5img class="anchor" src="icons/tick.png" id="bigop_Strue"\ 6lemma bigop_Strue: ∀k,p,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. p k \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
  73   \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
  74     op (f k) (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)).
  75 #k #p #B #nil #op #f #H normalize >H // qed.
  76
  77 \ 5img class="anchor" src="icons/tick.png" id="bigop_Sfalse"\ 6lemma bigop_Sfalse: ∀k,p,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. p k \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 →
  78   \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{ i < \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
  79     \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
  80 #k #p #B #nil #op #f #H normalize >H // qed.
  81
  82 \ 5img class="anchor" src="icons/tick.png" id="same_bigop"\ 6lemma same_bigop : ∀k,p1,p2,B,nil,op.∀f,g:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
  83   \ 5a href="cic:/matita/arithmetics/bigops/sameF_upto.def(2)"\ 6sameF_upto\ 5/a\ 6 k \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 p1 p2 → \ 5a href="cic:/matita/arithmetics/bigops/sameF_p.def(2)"\ 6sameF_p\ 5/a\ 6 k p1 B f g →
  84   \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < k | p1 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
  85     \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < k | p2 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(g i).
  86 #k #p1 #p2 #B #nil #op #f #g (elim k) //
  87 #n #Hind #samep #samef normalize >Hind
  88   [|@(\ 5a href="cic:/matita/arithmetics/bigops/sameF_p_le.def(5)"\ 6sameF_p_le\ 5/a\ 6 … samef) // |@(\ 5a href="cic:/matita/arithmetics/bigops/sameF_upto_le.def(5)"\ 6sameF_upto_le\ 5/a\ 6 … samep) //]
  89 <(samep … (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6 …)) cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p1 n)) #H1 >H1
  90 normalize // <(samef … (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6 …) H1) //
  91 qed.
  92
  93 \ 5img class="anchor" src="icons/tick.png" id="pad_bigop"\ 6theorem pad_bigop: ∀k,n,p,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 k →
  94 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < n | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)
  95   \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < k | \ 5font class="Apple-style-span" color="#FF0000"\ 6if\ 5/font\ 6 (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n i) then \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 else p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
  96 #k #n #p #B #nil #op #f #lenk (elim lenk)
  97   [@\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 #i #lti // >(\ 5a href="cic:/matita/arithmetics/nat/not_le_to_leb_false.def(7)"\ 6not_le_to_leb_false\ 5/a\ 6 …) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  98   |#j #leup #Hind >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 >(\ 5a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"\ 6le_to_leb_true\ 5/a\ 6 … leup) //
  99   ] qed.
 100
 101 \ 5img class="anchor" src="icons/tick.png" id="pad_bigop1"\ 6theorem pad_bigop1: ∀k,n,p,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 k →
 102   (∀i. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 k → p i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) →
 103   \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < n | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)
 104     \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
 105 #k #n #p #B #nil #op #f #lenk (elim lenk)
 106   [#_ @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 #i #lti //
 107   |#j #leup #Hind #Hfalse >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6
 108     [@Hind #i #leni #ltij @Hfalse // @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 //
 109     |@Hfalse //
 110     ]
 111   ]
 112 qed.
 113
 114 \ 5img class="anchor" src="icons/tick.png" id="bigop_false"\ 6theorem bigop_false: ∀n,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
 115   \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < n | \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 nil.
 116 #n #B #nil #op #f elim n // #n1 #Hind
 117 >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 //
 118 qed.
 119
 120 \ 5img class="anchor" src="icons/tick.png" id="Aop"\ 6record Aop (A:Type[0]) (nil:A) : Type[0] ≝
 121   {op :2> A → A → A;
 122    nill:∀a. op nil a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
 123    nilr:∀a. op a nil \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
 124    assoc: ∀a,b,c.op a (op b c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 op (op a b) c
 125   }.
 126
 127 \ 5img class="anchor" src="icons/tick.png" id="pad_bigop_nil"\ 6theorem pad_bigop_nil: ∀k,n,p,B,nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 k →
 128   (∀i. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 k → p i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 nil) →
 129   \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < n | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)
 130     \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
 131 #k #n #p #B #nil #op #f #lenk (elim lenk)
 132   [#_ @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 #i #lti //
 133   |#j #leup #Hind #Hfalse cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p j)) #Hpj
 134     [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 //
 135      cut (f j \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 nil)
 136       [cases (Hfalse j leup (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6 … )) // >Hpj #H destruct (H)] #Hfj
 137      >Hfj >\ 5a href="cic:/matita/arithmetics/bigops/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6 @Hind #i #leni #ltij
 138      cases (Hfalse i leni (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 … ltij)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 139     |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // @Hind #i #leni #ltij
 140      cases (Hfalse i leni (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 … ltij)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 141     ]
 142   ]
 143 qed.
 144
 145 \ 5img class="anchor" src="icons/tick.png" id="bigop_sum"\ 6theorem bigop_sum: ∀k1,k2,p1,p2,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f,g:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
 146 op (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k1|p1 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)) \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k2|p2 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(g i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 147       \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k1\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6k2|\ 5font class="Apple-style-span" color="#FF0000"\ 6 if \ 5/font\ 6\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 k2 i then p1 (i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6k2) else p2 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6
 148         (if \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 k2 i then f (i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6k2) else g i).
 149 #k1 #k2 #p1 #p2 #B #nil #op #f #g (elim k1)
 150   [normalize >\ 5a href="cic:/matita/arithmetics/bigops/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 #i #lti
 151    >(\ 5a href="cic:/matita/arithmetics/nat/lt_to_leb_false.def(8)"\ 6lt_to_leb_false\ 5/a\ 6 … lti) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 152   |#i #Hind normalize <\ 5a href="cic:/matita/arithmetics/nat/minus_plus_m_m.def(6)"\ 6minus_plus_m_m\ 5/a\ 6 (cases (p1 i))
 153    >(\ 5a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"\ 6le_to_leb_true\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/le_plus_n.def(7)"\ 6le_plus_n\ 5/a\ 6 …)) normalize <Hind //
 154    <\ 5a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 //
 155   ]
 156 qed.
 157
 158 \ 5img class="anchor" src="icons/tick.png" id="plus_minus1"\ 6lemma plus_minus1: ∀a,b,c. c \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b → a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6c.
 159 #a #b #c #lecb @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"\ 6plus_to_minus\ 5/a\ 6 >(\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 c)
 160 >\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 //
 161 qed.
 162
 163 \ 5img class="anchor" src="icons/tick.png" id="bigop_I"\ 6theorem bigop_I: ∀n,p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
 164 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i∈[\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6,n[ |p i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < n|p i}(f i).
 165 #n #p #B #nil #op #f <\ 5a href="cic:/matita/arithmetics/nat/minus_n_O.def(3)"\ 6minus_n_O\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 //
 166 qed.
 167
 168 \ 5img class="anchor" src="icons/tick.png" id="bigop_I_gen"\ 6theorem bigop_I_gen: ∀a,b,p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6b →
 169 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i∈[a,b[ |p i}(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < b|\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 a i \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 p i}(f i).
 170 #a #b elim b // -b #b #Hind #p #B #nil #op #f #lea
 171 cut (∀a,b. a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6a))
 172   [#a #b cases a // #a1 #lta1 normalize >\ 5a href="cic:/matita/arithmetics/nat/eq_minus_S_pred.def(4)"\ 6eq_minus_S_pred\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/nat/S_pred.def(3)"\ 6S_pred\ 5/a\ 6
 173    /2 by \ 5a href="cic:/matita/arithmetics/nat/lt_plus_to_minus_r.def(11)"\ 6lt_plus_to_minus_r\ 5/a\ 6/] #Hcut
 174 cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … lea) #Ha
 175   [cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p b)) #Hcase
 176     [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 [2: >Hcase >(\ 5a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"\ 6le_to_leb_true\ 5/a\ 6 a b) // @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @Ha]
 177      >(Hcut … (\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 … Ha))
 178      >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6
 179       [@\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6
 180         [@\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 [//|@\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 //] @Hind
 181         |@Hind @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 //
 182         ]
 183       |<\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 // @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 //
 184       ]
 185    |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 [2: >Hcase cases (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 a b)//]
 186      >(Hcut … (\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 … Ha)) >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6
 187       [@Hind @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 // | <\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 // @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 //]
 188     ]
 189   |<Ha <\ 5a href="cic:/matita/arithmetics/nat/minus_n_n.def(4)"\ 6minus_n_n\ 5/a\ 6 whd in ⊢ (??%?); <(\ 5a href="cic:/matita/arithmetics/bigops/bigop_false.def(4)"\ 6bigop_false\ 5/a\ 6 a B nil op f) in ⊢ (??%?);
 190    @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 // #i #ltia >(\ 5a href="cic:/matita/arithmetics/nat/not_le_to_leb_false.def(7)"\ 6not_le_to_leb_false\ 5/a\ 6 a i) // @\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6 //
 191   ]
 192 qed.
 193
 194 \ 5img class="anchor" src="icons/tick.png" id="bigop_sumI"\ 6theorem bigop_sumI: ∀a,b,c,p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
 195 a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b → b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 c →
 196 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i∈[a,c[ |p i}(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 197   op (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i ∈ [b,c[ |p i}(f i))
 198       \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i ∈ [a,b[ |p i}(f i).
 199 #a #b # c #p #B #nil #op #f #leab #lebc
 200 >(\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 (c\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6a) (b\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6a)) in ⊢ (??%?); /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(9)"\ 6monotonic_le_minus_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 201 >\ 5a href="cic:/matita/arithmetics/nat/minus_plus.def(13)"\ 6minus_plus\ 5/a\ 6 >(\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 a) <\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 //
 202 >\ 5a href="cic:/matita/arithmetics/bigops/bigop_sum.def(9)"\ 6bigop_sum\ 5/a\ 6 (cut (∀i. b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → i\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6(b\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6a)\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6b))
 203   [#i #lei >\ 5a href="cic:/matita/arithmetics/nat/plus_minus.def(5)"\ 6plus_minus\ 5/a\ 6 // <\ 5a href="cic:/matita/arithmetics/bigops/plus_minus1.def(8)"\ 6plus_minus1\ 5/a\ 6
 204      [@\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"\ 6plus_to_minus\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/bigops/plus_minus1.def(8)"\ 6plus_minus1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(9)"\ 6monotonic_le_minus_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]]
 205 #H @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 #i #ltic @\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 normalize // #lei <H //
 206 qed.
 207
 208 \ 5img class="anchor" src="icons/tick.png" id="bigop_a"\ 6theorem bigop_a: ∀a,b,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b →
 209 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i∈[a,\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b[ }(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 210   op (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i ∈ [a,b[ }(f (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i))) (f a).
 211 #a #b #B #nil #op #f #leab
 212 >(\ 5a href="cic:/matita/arithmetics/bigops/bigop_sumI.def(14)"\ 6bigop_sumI\ 5/a\ 6 a (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 a) (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b)) [|@\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 //|//] @\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6
 213   [@\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 // |<\ 5a href="cic:/matita/arithmetics/nat/minus_Sn_n.def(4)"\ 6minus_Sn_n\ 5/a\ 6 normalize @\ 5a href="cic:/matita/arithmetics/bigops/nilr.fix(0,2,2)"\ 6nilr\ 5/a\ 6]
 214 qed.
 215
 216 \ 5img class="anchor" src="icons/tick.png" id="bigop_0"\ 6theorem bigop_0: ∀n,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
 217 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n}(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 218   op (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < n}(f (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i))) (f \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6).
 219 #n #B #nil #op #f
 220 <\ 5a href="cic:/matita/arithmetics/bigops/bigop_I.def(7)"\ 6bigop_I\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/bigops/bigop_a.def(15)"\ 6bigop_a\ 5/a\ 6 [|//] @\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6 [|//] <\ 5a href="cic:/matita/arithmetics/nat/minus_n_O.def(3)"\ 6minus_n_O\ 5/a\ 6
 221 @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 //
 222 qed.
 223
 224 \ 5img class="anchor" src="icons/tick.png" id="bigop_prod"\ 6theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 →\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → B.
 225 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{x<k1|p1 x}(\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k2|p2 x i}(f x i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 226   \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k1\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6k2|\ 5a href="cic:/matita/basics/bool/andb.def(1)"\ 6andb\ 5/a\ 6 (p1 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 i k2)) (p2 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 i k2) (i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 k2))}
 227      (f (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 i k2) (i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 k2)).
 228 #k1 #k2 #p1 #p2 #B #nil #op #f (elim k1) //
 229 #n #Hind cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p1 n)) #Hp1
 230   [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >Hind >\ 5a href="cic:/matita/arithmetics/bigops/bigop_sum.def(9)"\ 6bigop_sum\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6
 231    #i #lti @\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 // #lei cut (i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6k2\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6k2)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/bigops/plus_minus1.def(8)"\ 6plus_minus1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 232    #eqi [|#H] >eqi in ⊢ (???%);
 233      >\ 5a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"\ 6div_plus_times\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_plus_to_lt_l.def(6)"\ 6lt_plus_to_lt_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ >Hp1 >(\ 5a href="cic:/matita/arithmetics/div_and_mod/mod_plus_times.def(14)"\ 6mod_plus_times\ 5/a\ 6 …) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/nat/lt_plus_to_lt_l.def(6)"\ 6lt_plus_to_lt_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 234   |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // >Hind >(\ 5a href="cic:/matita/arithmetics/bigops/pad_bigop.def(8)"\ 6pad_bigop\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6k2)) // @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6
 235    #i #lti @\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 // #lei cut (i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6k2\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6k2)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/bigops/plus_minus1.def(8)"\ 6plus_minus1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 236    #eqi >eqi in ⊢ (???%); >\ 5a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"\ 6div_plus_times\ 5/a\ 6 [ >Hp1 %| /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_minus_l.def(12)"\ 6monotonic_lt_minus_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
 237   ]
 238 qed.
 239
 240 \ 5img class="anchor" src="icons/tick.png" id="ACop"\ 6record ACop (A:Type[0]) (nil:A) : Type[0] ≝
 241   {aop :> \ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 A nil;
 242    comm: ∀a,b.aop a b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 aop b a
 243   }.
 244
 245 \ 5img class="anchor" src="icons/tick.png" id="bigop_op"\ 6lemma bigop_op: ∀k,p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"\ 6ACop\ 5/a\ 6 B nil.∀f,g: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → B.
 246 op (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k|p i}(f i)) (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k|p i}(g i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 247   \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k|p i}(op (f i) (g i)).
 248 #k #p #B #nil #op #f #g (elim k) [normalize @\ 5a href="cic:/matita/arithmetics/bigops/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6]
 249 -k #k #Hind (cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p k))) #H
 250   [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 //
 251    normalize <\ 5a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 in ⊢ (???%); @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6
 252    >\ 5a href="cic:/matita/arithmetics/bigops/comm.fix(0,2,3)"\ 6comm\ 5/a\ 6 in ⊢ (??(????%?)?); <\ 5a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 @Hind
 253   |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 //
 254   ]
 255 qed.
 256
 257 \ 5img class="anchor" src="icons/tick.png" id="bigop_diff"\ 6lemma bigop_diff: ∀p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"\ 6ACop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → B.∀i,n.
 258   i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → p i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
 259   \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{x<n|p x}(f x)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 260     op (f i) (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{x<n|\ 5a href="cic:/matita/basics/bool/andb.def(1)"\ 6andb\ 5/a\ 6(\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 i x))(p x)}(f x)).
 261 #p #B #nil #op #f #i #n (elim n)
 262   [#ltO @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 263   |#n #Hind #lein #pi cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 …lein)) #Hi
 264     [cut (\ 5a href="cic:/matita/basics/bool/andb.def(1)"\ 6andb\ 5/a\ 6(\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 i n))(p n) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (p n))
 265       [>(\ 5a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"\ 6not_eq_to_eqb_false\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"\ 6lt_to_not_eq\ 5/a\ 6 … Hi)) //] #Hcut
 266      cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p n)) #pn
 267       [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 //
 268        normalize >\ 5a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 >(\ 5a href="cic:/matita/arithmetics/bigops/comm.fix(0,2,3)"\ 6comm\ 5/a\ 6 ?? op (f i) (f n)) <\ 5a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 >Hind //
 269       |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // >Hind //
 270       ]
 271     |<Hi >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6
 272        [@\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 // #k #ltki >\ 5a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"\ 6not_eq_to_eqb_false\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 273        |>\ 5a href="cic:/matita/arithmetics/nat/eq_to_eqb_true.def(5)"\ 6eq_to_eqb_true\ 5/a\ 6 //
 274        ]
 275      ]
 276    ]
 277 qed.
 278
 279 (* range *)
 280 \ 5img class="anchor" src="icons/tick.png" id="range"\ 6record range (A:Type[0]): Type[0] ≝
 281   {enum:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→A; upto:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6; filter:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6}.
 282
 283 \ 5img class="anchor" src="icons/tick.png" id="sub_hk"\ 6definition sub_hk: (\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6)→(\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6)→∀A:Type[0].\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/bigops/range.ind(1,0,1)"\ 6range\ 5/a\ 6 A) ≝
 284 λh,k,A,I,J.∀i.i\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"\ 6upto\ 5/a\ 6 A I) → (\ 5a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"\ 6filter\ 5/a\ 6 A I i)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
 285   (h i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"\ 6upto\ 5/a\ 6 A J
 286   \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"\ 6filter\ 5/a\ 6 A J (h i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
 287   \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 k (h i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 i).
 288
 289 \ 5img class="anchor" src="icons/tick.png" id="iso"\ 6definition iso: ∀A:Type[0].\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/bigops/range.ind(1,0,1)"\ 6range\ 5/a\ 6 A) ≝
 290   λA,I,J.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6h,k\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6
 291     (∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"\ 6upto\ 5/a\ 6 A I) → (\ 5a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"\ 6filter\ 5/a\ 6 A I i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
 292        \ 5a href="cic:/matita/arithmetics/bigops/enum.fix(0,1,1)"\ 6enum\ 5/a\ 6 A I i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigops/enum.fix(0,1,1)"\ 6enum\ 5/a\ 6 A J (h i)) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6
 293     \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 h k A I J \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 k h A J I.
 294
 295 \ 5img class="anchor" src="icons/tick.png" id="sub_hkO"\ 6lemma sub_hkO: ∀h,k,A,I,J. \ 5a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"\ 6upto\ 5/a\ 6 A I \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 h k A I J.
 296 #h #k #A #I #J #up0 #i #lti >up0 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 297 qed.
 298
 299 \ 5img class="anchor" src="icons/tick.png" id="sub0_to_false"\ 6lemma sub0_to_false: ∀h,k,A,I,J. \ 5a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"\ 6upto\ 5/a\ 6 A I \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 h k A J I →
 300   ∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"\ 6upto\ 5/a\ 6 A J → \ 5a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"\ 6filter\ 5/a\ 6 A J i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
 301 #h #k #A #I #J #up0 #sub #i #lti cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"\ 6filter\ 5/a\ 6 A J i)) //
 302 #ptrue (cases (sub i lti ptrue)) * #hi @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 303 qed.
 304
 305 \ 5img class="anchor" src="icons/tick.png" id="sub_lt"\ 6lemma sub_lt: ∀A,e,p,n,m. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m →
 306   \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 (λx.x) (λx.x) A (\ 5a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"\ 6mk_range\ 5/a\ 6 A e n p) (\ 5a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"\ 6mk_range\ 5/a\ 6 A e m p).
 307 #A #e #f #n #m #lenm #i #lti #fi % // % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 308 qed.
 309
 310 \ 5img class="anchor" src="icons/tick.png" id="transitive_sub"\ 6theorem transitive_sub: ∀h1,k1,h2,k2,A,I,J,K.
 311   \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 h1 k1 A I J → \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 h2 k2 A J K →
 312     \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 (λx.h2(h1 x)) (λx.k1(k2 x)) A I K.
 313 #h1 #k1 #h2 #k2 #A #I #J #K #sub1 #sub2 #i #lti #fi
 314 cases(sub1 i lti fi) * #lth1i #fh1i #ei
 315 cases(sub2 (h1 i) lth1i fh1i) * #H1 #H2 #H3 % // % //
 316 qed.
 317
 318 \ 5img class="anchor" src="icons/tick.png" id="bigop_iso"\ 6theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"\ 6ACop\ 5/a\ 6 B nil.∀f1,f2.
 319   \ 5a href="cic:/matita/arithmetics/bigops/iso.def(3)"\ 6iso\ 5/a\ 6 B (\ 5a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"\ 6mk_range\ 5/a\ 6 B f1 n1 p1) (\ 5a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"\ 6mk_range\ 5/a\ 6 B f2 n2 p2) →
 320   \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<n1|p1 i}(f1 i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<n2|p2 i}(f2 i).
 321 #n1 #n2 #p1 #p2 #B #nil #op #f1 #f2 * #h * #k * * #same
 322 @(\ 5a href="cic:/matita/arithmetics/nat/le_gen.def(1)"\ 6le_gen\ 5/a\ 6 ? n1) #i generalize in match p2; (elim i)
 323   [(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
 324    >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6
 325     [@(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) //]
 326     |@(\ 5a href="cic:/matita/arithmetics/bigops/sub0_to_false.def(4)"\ 6sub0_to_false\ 5/a\ 6 … sub2) //
 327     ]
 328   |#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
 329    cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p1 n)) #p1n
 330     [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // (cases (sub1 n (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6 …) p1n)) * #hn #p2hn #eqn
 331      >(\ 5a href="cic:/matita/arithmetics/bigops/bigop_diff.def(8)"\ 6bigop_diff\ 5/a\ 6 … (h n) n2) // >same //
 332      @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 @(Hind ? len)
 333       [#i #ltin #p1i (cases (sub1 i (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 … ltin) p1i)) *
 334        #h1i #p2h1i #eqi % // % // >\ 5a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"\ 6not_eq_to_eqb_false\ 5/a\ 6 normalize //
 335        @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 ??? (\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"\ 6lt_to_not_eq\ 5/a\ 6 ? ? ltin)) //
 336       |#j #ltj #p2j (cases (sub2 j ltj (\ 5a href="cic:/matita/basics/bool/andb_true_r.def(4)"\ 6andb_true_r\ 5/a\ 6 …p2j))) *
 337        #ltkj #p1kj #eqj % // % //
 338        (cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 …(\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 …ltkj))) //
 339        #eqkj @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 generalize in match p2j; @\ 5a href="cic:/matita/arithmetics/nat/eqb_elim.def(5)"\ 6eqb_elim\ 5/a\ 6
 340        normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 341       ]
 342     |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // @(Hind ? len)
 343       [@(\ 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 …) sub1) //
 344       |#i #lti #p2i cases(sub2 i lti p2i) * #ltki #p1ki #eqi
 345        % // % // cases(\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 …(\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 …ltki)) //
 346        #eqki @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 347       ]
 348     ]
 349   ]
 350 qed.
 351
 352 (* commutation *)
 353 \ 5img class="anchor" src="icons/tick.png" id="bigop_commute"\ 6theorem bigop_commute: ∀n,m,p11,p12,p21,p22,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"\ 6ACop\ 5/a\ 6 B nil.∀f.
 354 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m →
 355 (∀i,j. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → j \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → (p11 i \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 p12 i j) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (p21 j \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 p22 i j)) →
 356 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<n|p11 i}(\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{j<m|p12 i j}(f i j)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 357    \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{j<m|p21 j}(\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<n|p22 i j}(f i j)).
 358 #n #m #p11 #p12 #p21 #p22 #B #nil #op #f #posn #posm #Heq
 359 >\ 5a href="cic:/matita/arithmetics/bigops/bigop_prod.def(15)"\ 6bigop_prod\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/bigops/bigop_prod.def(15)"\ 6bigop_prod\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/bigops/bigop_iso.def(9)"\ 6bigop_iso\ 5/a\ 6
 360 %{(λi.(i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m)} %{(λi.(i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n)} %
 361   [%
 362     [#i #lti #Heq (* whd in ⊢ (???(?(?%?)?)); *) @\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6
 363       [@\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/mod_plus_times.def(14)"\ 6mod_plus_times\ 5/a\ 6 /2 by \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6/
 364       |@\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"\ 6div_plus_times\ 5/a\ 6 /2 by \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6/
 365       ]
 366     |#i #lti #Hi
 367      cut ((i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m)\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m)
 368       [@\ 5a href="cic:/matita/arithmetics/div_and_mod/mod_plus_times.def(14)"\ 6mod_plus_times\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 //] #H1
 369      cut ((i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m)
 370       [@\ 5a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"\ 6div_plus_times\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 //] #H2
 371      %[%[@(\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6 ? (i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n))
 372           [whd >\ 5a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"\ 6plus_n_Sm\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"\ 6monotonic_le_plus_r\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 //
 373           |>\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 @(\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m)) m n n) // @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 //
 374           ]
 375         |lapply (Heq (i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m) (i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m) ??)
 376           [@\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 // |@\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 //|>Hi >H1 >H2 //]
 377         ]
 378       |>H1 >H2 //
 379       ]
 380     ]
 381   |#i #lti #Hi
 382    cut ((i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n)\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n)
 383     [@\ 5a href="cic:/matita/arithmetics/div_and_mod/mod_plus_times.def(14)"\ 6mod_plus_times\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 //] #H1
 384    cut ((i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n)
 385     [@\ 5a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"\ 6div_plus_times\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 //] #H2
 386    %[%[@(\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6 ? (i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m))
 387         [whd >\ 5a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"\ 6plus_n_Sm\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"\ 6monotonic_le_plus_r\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 //
 388         |>\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 @(\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n)) n m m) // @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 //
 389         ]
 390       |lapply (Heq (i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n) (i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n) ??)
 391         [@\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 // |@\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 // |>Hi >H1 >H2 //]
 392       ]
 393     |>H1 >H2 //
 394     ]
 395   ]
 396 qed.
 397
 398 (* distributivity *)
 399
 400 \ 5img class="anchor" src="icons/tick.png" id="Dop"\ 6record Dop (A:Type[0]) (nil:A): Type[0] ≝
 401   {sum : \ 5a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"\ 6ACop\ 5/a\ 6 A nil;
 402    prod: A → A →A;
 403    null: \forall a. prod a nil \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 nil;
 404    distr: ∀a,b,c:A. prod a (sum b c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 sum (prod a b) (prod a c)
 405   }.
 406
 407 \ 5img class="anchor" src="icons/tick.png" id="bigop_distr"\ 6theorem bigop_distr: ∀n,p,B,nil.∀R:\ 5a href="cic:/matita/arithmetics/bigops/Dop.ind(1,0,2)"\ 6Dop\ 5/a\ 6 B nil.\forall f,a.
 408   let aop \def  \ 5a href="cic:/matita/arithmetics/bigops/sum.fix(0,2,4)"\ 6sum\ 5/a\ 6 B nil R in
 409   let mop \def \ 5a href="cic:/matita/arithmetics/bigops/prod.fix(0,2,4)"\ 6prod\ 5/a\ 6 B nil R in
 410   mop a \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[aop,nil]_{i<n|p i}(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 411    \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[aop,nil]_{i<n|p i}(mop a (f i)).
 412 #n #p #B #nil #R #f #a normalize (elim n) [@\ 5a href="cic:/matita/arithmetics/bigops/null.fix(0,2,5)"\ 6null\ 5/a\ 6]
 413 #n #Hind (cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p n))) #H
 414   [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >(\ 5a href="cic:/matita/arithmetics/bigops/distr.fix(0,2,5)"\ 6distr\ 5/a\ 6 B nil R) >Hind //
 415   |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 //
 416   ]
 417 qed.
 418