#a #b #B #nil #op #f #leab
>(\ 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
[@\ 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]
qed.
\ 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.
#a #b #B #nil #op #f #leab
>(\ 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
[@\ 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]
qed.
\ 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.