matita/library/nat/iteration2.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/iteration2".
  16
  17 include "nat/primes.ma".
  18 include "nat/ord.ma".
  19 include "nat/generic_iter_p.ma".
  20 include "nat/count.ma".(*necessary just to use bool_to_nat and bool_to_nat_andb*)
  21
  22
  23 (* sigma_p on nautral numbers is a specialization of sigma_p_gen *)
  24 definition sigma_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
  25 \lambda n, p, g. (iter_p_gen n p nat g O plus).
  26
  27 theorem symmetricIntPlus: symmetric nat plus.
  28 change with (\forall a,b:nat. (plus a b) = (plus b a)).
  29 intros.
  30 rewrite > sym_plus.
  31 reflexivity.
  32 qed.
  33
  34 (*the following theorems on sigma_p in N are obtained by the more general ones
  35  * in sigma_p_gen.ma
  36  *)
  37 theorem true_to_sigma_p_Sn:
  38 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
  39 p n = true \to sigma_p (S n) p g =
  40 (g n)+(sigma_p n p g).
  41 intros.
  42 unfold sigma_p.
  43 apply true_to_iter_p_gen_Sn.
  44 assumption.
  45 qed.
  46
  47 theorem false_to_sigma_p_Sn:
  48 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
  49 p n = false \to sigma_p (S n) p g = sigma_p n p g.
  50 intros.
  51 unfold sigma_p.
  52 apply false_to_iter_p_gen_Sn.
  53 assumption.
  54 qed.
  55
  56 theorem eq_sigma_p: \forall p1,p2:nat \to bool.
  57 \forall g1,g2: nat \to nat.\forall n.
  58 (\forall x.  x < n \to p1 x = p2 x) \to
  59 (\forall x.  x < n \to g1 x = g2 x) \to
  60 sigma_p n p1 g1 = sigma_p n p2 g2.
  61 intros.
  62 unfold sigma_p.
  63 apply eq_iter_p_gen;
  64   assumption.
  65 qed.
  66
  67 theorem eq_sigma_p1: \forall p1,p2:nat \to bool.
  68 \forall g1,g2: nat \to nat.\forall n.
  69 (\forall x.  x < n \to p1 x = p2 x) \to
  70 (\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
  71 sigma_p n p1 g1 = sigma_p n p2 g2.
  72 intros.
  73 unfold sigma_p.
  74 apply eq_iter_p_gen1;
  75   assumption.
  76 qed.
  77
  78 theorem sigma_p_false:
  79 \forall g: nat \to nat.\forall n.sigma_p n (\lambda x.false) g = O.
  80 intros.
  81 unfold sigma_p.
  82 apply iter_p_gen_false.
  83 qed.
  84
  85 theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
  86 \forall g: nat \to nat.
  87 sigma_p (k+n) p g
  88 = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
  89 intros.
  90 unfold sigma_p.
  91 apply (iter_p_gen_plusA nat n k p g O plus)
  92 [ apply symmetricIntPlus.
  93 | intros.
  94   apply sym_eq.
  95   apply plus_n_O
  96 | apply associative_plus
  97 ]
  98 qed.
  99
 100 theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to
 101 \forall p:nat \to bool.
 102 \forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
 103 p i = false) \to sigma_p m p g = sigma_p n p g.
 104 intros.
 105 unfold sigma_p.
 106 apply (false_to_eq_iter_p_gen);
 107   assumption.
 108 qed.
 109
 110 theorem sigma_p2 :
 111 \forall n,m:nat.
 112 \forall p1,p2:nat \to bool.
 113 \forall g: nat \to nat \to nat.
 114 sigma_p (n*m)
 115   (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
 116   (\lambda x.g (div x m) (mod x m)) =
 117 sigma_p n p1
 118   (\lambda x.sigma_p m p2 (g x)).
 119 intros.
 120 unfold sigma_p.
 121 apply (iter_p_gen2 n m p1 p2 nat g O plus)
 122 [ apply symmetricIntPlus
 123 | apply associative_plus
 124 | intros.
 125   apply sym_eq.
 126   apply plus_n_O
 127 ]
 128 qed.
 129
 130 theorem sigma_p2' :
 131 \forall n,m:nat.
 132 \forall p1:nat \to bool.
 133 \forall p2:nat \to nat \to bool.
 134 \forall g: nat \to nat \to nat.
 135 sigma_p (n*m)
 136   (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x  m)))
 137   (\lambda x.g (div x m) (mod x m)) =
 138 sigma_p n p1
 139   (\lambda x.sigma_p m (p2 x) (g x)).
 140 intros.
 141 unfold sigma_p.
 142 apply (iter_p_gen2' n m p1 p2 nat g O plus)
 143 [ apply symmetricIntPlus
 144 | apply associative_plus
 145 | intros.
 146   apply sym_eq.
 147   apply plus_n_O
 148 ]
 149 qed.
 150
 151 lemma sigma_p_gi: \forall g: nat \to nat.
 152 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
 153 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
 154 intros.
 155 unfold sigma_p.
 156 apply (iter_p_gen_gi)
 157 [ apply symmetricIntPlus
 158 | apply associative_plus
 159 | intros.
 160   apply sym_eq.
 161   apply plus_n_O
 162 | assumption
 163 | assumption
 164 ]
 165 qed.
 166
 167 theorem eq_sigma_p_gh:
 168 \forall g,h,h1: nat \to nat.\forall n,n1.
 169 \forall p1,p2:nat \to bool.
 170 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
 171 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
 172 (\forall i. i < n \to p1 i = true \to h i < n1) \to
 173 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
 174 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
 175 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
 176 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 p2 g.
 177 intros.
 178 unfold sigma_p.
 179 apply (eq_iter_p_gen_gh nat O plus ? ? ? g h h1 n n1 p1 p2)
 180 [ apply symmetricIntPlus
 181 | apply associative_plus
 182 | intros.
 183   apply sym_eq.
 184   apply plus_n_O
 185 | assumption
 186 | assumption
 187 | assumption
 188 | assumption
 189 | assumption
 190 | assumption
 191 ]
 192 qed.
 193
 194
 195 theorem sigma_p_divides:
 196 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
 197 \forall g: nat \to nat.
 198 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
 199 sigma_p (S n) (\lambda x.divides_b x n)
 200   (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
 201 intros.
 202 unfold sigma_p.
 203 apply (iter_p_gen_divides nat O plus n m p ? ? ? g)
 204 [ assumption
 205 | assumption
 206 | assumption
 207 | apply symmetricIntPlus
 208 | apply associative_plus
 209 | intros.
 210   apply sym_eq.
 211   apply plus_n_O
 212 ]
 213 qed.
 214
 215 theorem distributive_times_plus_sigma_p: \forall n,k:nat. \forall p:nat \to bool. \forall g:nat \to nat.
 216 k*(sigma_p n p g) = sigma_p n p (\lambda i:nat.k * (g i)).
 217 intros.
 218 apply (distributive_times_plus_iter_p_gen nat plus O times n k p g)
 219 [ apply symmetricIntPlus
 220 | apply associative_plus
 221 | intros.
 222   apply sym_eq.
 223   apply plus_n_O
 224 | apply symmetric_times
 225 | apply distributive_times_plus
 226 | intros.
 227   rewrite < (times_n_O a).
 228   reflexivity
 229 ]
 230 qed.
 231
 232 (*some properties of sigma_p invoked with an "always true" predicate (in this
 233   way sigma_p just counts the elements, without doing any control) or with
 234   the nat \to nat function which always returns (S O).
 235   It 's not easily possible proving these theorems in a general form
 236   in generic_sigma_p.ma
 237  *)
 238
 239 theorem sigma_p_true: \forall n:nat.
 240 (sigma_p n (\lambda x.true) (\lambda x.S O)) = n.
 241 intros.
 242 elim n
 243 [ simplify.
 244   reflexivity
 245 | rewrite > (true_to_sigma_p_Sn n1 (\lambda x:nat.true) (\lambda x:nat.S O))
 246   [ rewrite > H.
 247     simplify.
 248     reflexivity
 249   | reflexivity
 250   ]
 251 ]
 252 qed.
 253
 254 theorem sigma_P_SO_to_sigma_p_true: \forall n:nat. \forall g:nat \to bool.
 255 sigma_p n g (\lambda n:nat. (S O)) =
 256 sigma_p n (\lambda x:nat.true) (\lambda i:nat.bool_to_nat (g i)).
 257 intros.
 258 elim n
 259 [ simplify.
 260   reflexivity
 261 | cut ((g n1) = true \lor (g n1) = false)
 262   [ rewrite > true_to_sigma_p_Sn in \vdash (? ? ? %)
 263     [ elim Hcut
 264       [ rewrite > H1.
 265         rewrite > true_to_sigma_p_Sn in \vdash (? ? % ?)
 266         [ simplify.
 267           apply eq_f.
 268           assumption
 269         | assumption
 270         ]
 271       | rewrite > H1.
 272         rewrite > false_to_sigma_p_Sn in \vdash (? ? % ?)
 273         [ simplify.
 274           assumption
 275         | assumption
 276         ]
 277       ]
 278     | reflexivity
 279     ]
 280   | elim (g n1)
 281     [ left.
 282       reflexivity
 283     | right.
 284       reflexivity
 285     ]
 286   ]
 287 ]
 288 qed.
 289
 290 (* I introduce an equivalence in the form map_iter_i in order to use
 291  * the existing result about permutation in that part of the library.
 292  *)
 293
 294 theorem eq_map_iter_i_sigma_p_alwaysTrue:  \forall n:nat.\forall g:nat \to nat.
 295 map_iter_i n g plus O = sigma_p (S n) (\lambda c:nat.true) g.
 296 intros.
 297 elim n
 298 [ simplify.
 299   rewrite < plus_n_O.
 300   reflexivity
 301 | rewrite > true_to_sigma_p_Sn
 302   [ simplify in \vdash (? ? % ?).
 303     rewrite < plus_n_O.
 304     apply eq_f.
 305     assumption
 306   | reflexivity
 307   ]
 308 ]
 309 qed.
 310
 311 theorem sigma_p_plus_1: \forall n:nat. \forall f,g:nat \to nat.
 312 sigma_p n (\lambda b:nat. true) (\lambda a:nat.(f a) + (g a)) =
 313 sigma_p n (\lambda b:nat. true) f + sigma_p n (\lambda b:nat. true) g.
 314 intros.
 315 elim n
 316 [ simplify.
 317   reflexivity
 318 | rewrite > true_to_sigma_p_Sn
 319   [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) f)
 320     [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) g)
 321       [ rewrite > assoc_plus in \vdash (? ? ? %).
 322         rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
 323         rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
 324         rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
 325         rewrite < assoc_plus in \vdash (? ? ? %).
 326         apply eq_f.
 327         assumption
 328       | reflexivity
 329       ]
 330     | reflexivity
 331     ]
 332   | reflexivity
 333   ]
 334 ]
 335 qed.
 336
 337
 338 theorem eq_sigma_p_sigma_p_times1 : \forall n,m:nat.\forall f:nat \to nat.
 339 sigma_p (n*m) (\lambda x:nat.true) f =
 340 sigma_p m (\lambda x:nat.true)
 341     (\lambda a.(sigma_p n (\lambda x:nat.true) (\lambda b.f (b*m + a)))).
 342 intro.
 343 elim n
 344 [ simplify.
 345   elim m
 346   [ simplify.
 347     reflexivity
 348   | rewrite > true_to_sigma_p_Sn
 349     [ rewrite < H.
 350       reflexivity
 351     | reflexivity
 352     ]
 353   ]
 354 | change in \vdash (? ? ? (? ? ? (\lambda a:?.%))) with ((f ((n1*m)+a)) +
 355   (sigma_p n1 (\lambda x:nat.true) (\lambda b:nat.f (b*m +a)))).
 356   rewrite > sigma_p_plus_1 in \vdash (? ? ? %).
 357   rewrite > (sym_times (S n1) m).
 358   rewrite < (times_n_Sm m  n1).
 359   rewrite > sigma_p_plus in \vdash (? ? % ?).
 360   apply eq_f2
 361   [ rewrite < (sym_times m n1).
 362     apply eq_sigma_p
 363     [ intros.
 364       reflexivity
 365     | intros.
 366       rewrite < (sym_plus ? (m * n1)).
 367       reflexivity
 368     ]
 369   | rewrite > (sym_times m n1).
 370     apply H
 371   ]
 372 ]
 373 qed.
 374
 375 theorem eq_sigma_p_sigma_p_times2 : \forall n,m:nat.\forall f:nat \to nat.
 376 sigma_p (n *m) (\lambda c:nat.true) f =
 377 sigma_p  n (\lambda c:nat.true)
 378   (\lambda a.(sigma_p m (\lambda c:nat.true) (\lambda b:nat.f (b* n + a)))).
 379 intros.
 380 rewrite > sym_times.
 381 apply eq_sigma_p_sigma_p_times1.
 382 qed.
 383
 384
 385 theorem sigma_p_times:\forall n,m:nat.
 386 \forall f,f1,f2:nat \to bool.
 387 \forall g:nat \to nat \to nat.
 388 \forall g1,g2: nat \to nat.
 389 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
 390 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
 391 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
 392 (\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
 393 (sigma_p ((S n) * (S m)) f (\lambda c:nat.(S O))) =
 394 sigma_p (S n) f1 (\lambda c:nat.(S O)) * sigma_p (S m) f2 (\lambda c:nat.(S O)).
 395 intros.
 396
 397 rewrite > (sigma_P_SO_to_sigma_p_true ).
 398 rewrite > (S_pred ((S n)*(S m))) in \vdash (? ? (? % ? ?) ?)
 399 [ rewrite < (eq_map_iter_i_sigma_p_alwaysTrue (pred ((S n)* (S m)))).
 400   rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ?
 401            (\lambda i.g (div i (S n)) (mod i (S n))))
 402   [ rewrite > eq_map_iter_i_sigma_p_alwaysTrue.
 403     rewrite < S_pred
 404     [ rewrite > eq_sigma_p_sigma_p_times2.
 405       apply (trans_eq ? ? (sigma_p (S n)  (\lambda c:nat.true)
 406         (\lambda a. sigma_p (S m) (\lambda c:nat.true)
 407                 (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))))))
 408       [ apply eq_sigma_p;intros
 409         [ reflexivity
 410         | apply eq_sigma_p;intros
 411           [ reflexivity
 412           |
 413             rewrite > (div_mod_spec_to_eq (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
 414                                                   ((x1*(S n) + x) \mod (S n)) x1 x)
 415             [ rewrite > (div_mod_spec_to_eq2 (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
 416                                                   ((x1*(S n) + x) \mod (S n)) x1 x)
 417               [ rewrite > H3
 418                 [ apply bool_to_nat_andb
 419                 | assumption
 420                 | assumption
 421                 ]
 422               | apply div_mod_spec_div_mod.
 423                 apply lt_O_S
 424               | constructor 1
 425                 [ assumption
 426                 | reflexivity
 427                 ]
 428               ]
 429             | apply div_mod_spec_div_mod.
 430               apply lt_O_S
 431             | constructor 1
 432               [ assumption
 433               | reflexivity
 434               ]
 435             ]
 436           ]
 437         ]
 438       | apply (trans_eq ? ?
 439          (sigma_p (S n) (\lambda c:nat.true) (\lambda n.((bool_to_nat (f1 n)) *
 440          (sigma_p (S m) (\lambda c:nat.true) (\lambda n.bool_to_nat (f2 n)))))))
 441         [ apply eq_sigma_p;intros
 442           [ reflexivity
 443           | rewrite > distributive_times_plus_sigma_p.
 444             apply eq_sigma_p;intros
 445             [ reflexivity
 446             | rewrite > sym_times.
 447               reflexivity
 448             ]
 449           ]
 450         | apply sym_eq.
 451           rewrite > sigma_P_SO_to_sigma_p_true.
 452           rewrite > sigma_P_SO_to_sigma_p_true in \vdash (? ? (? ? %) ?).
 453           rewrite > sym_times.
 454           rewrite > distributive_times_plus_sigma_p.
 455           apply eq_sigma_p;intros
 456           [ reflexivity
 457           | rewrite > distributive_times_plus_sigma_p.
 458             rewrite < sym_times.
 459             rewrite > distributive_times_plus_sigma_p.
 460             apply eq_sigma_p;
 461               intros; reflexivity
 462           ]
 463         ]
 464       ]
 465     | apply lt_O_times_S_S
 466     ]
 467
 468   | unfold permut.
 469     split
 470     [ intros.
 471       rewrite < plus_n_O.
 472       apply le_S_S_to_le.
 473       rewrite < S_pred in \vdash (? ? %)
 474       [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
 475         apply H
 476         [ apply lt_mod_m_m.
 477           unfold lt.
 478           apply le_S_S.
 479           apply le_O_n
 480         | apply (lt_times_to_lt_l n).
 481           apply (le_to_lt_to_lt ? i)
 482           [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
 483             [ rewrite > sym_plus.
 484               apply le_plus_n
 485             | unfold lt.
 486               apply le_S_S.
 487               apply le_O_n
 488             ]
 489           | unfold lt.
 490             rewrite > S_pred in \vdash (? ? %)
 491             [ apply le_S_S.
 492               rewrite > plus_n_O in \vdash (? ? %).
 493               rewrite > sym_times.
 494               assumption
 495             | apply lt_O_times_S_S
 496             ]
 497           ]
 498         ]
 499       | apply lt_O_times_S_S
 500       ]
 501     | rewrite < plus_n_O.
 502       unfold injn.
 503       intros.
 504       cut (i < (S n)*(S m))
 505       [ cut (j < (S n)*(S m))
 506         [ cut ((i \mod (S n)) < (S n))
 507           [ cut ((i/(S n)) < (S m))
 508             [ cut ((j \mod (S n)) < (S n))
 509               [ cut ((j/(S n)) < (S m))
 510                 [ rewrite > (div_mod i (S n))
 511                   [ rewrite > (div_mod j (S n))
 512                     [ rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
 513                       rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
 514                       rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
 515                       rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
 516                       rewrite > H6.
 517                       reflexivity
 518                     | unfold lt.
 519                       apply le_S_S.
 520                       apply le_O_n
 521                     ]
 522                   | unfold lt.
 523                     apply le_S_S.
 524                     apply le_O_n
 525                   ]
 526                 | apply (lt_times_to_lt_l n).
 527                   apply (le_to_lt_to_lt ? j)
 528                   [ rewrite > (div_mod j (S n)) in \vdash (? ? %)
 529                     [ rewrite > sym_plus.
 530                       apply le_plus_n
 531                     | unfold lt. apply le_S_S.
 532                       apply le_O_n
 533                     ]
 534                   | rewrite < sym_times.
 535                     assumption
 536                   ]
 537                 ]
 538               | apply lt_mod_m_m.
 539                 unfold lt.
 540                 apply le_S_S.
 541                 apply le_O_n
 542               ]
 543             | apply (lt_times_to_lt_l n).
 544               apply (le_to_lt_to_lt ? i)
 545               [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
 546                 [ rewrite > sym_plus.
 547                   apply le_plus_n
 548                 | unfold lt.
 549                   apply le_S_S.
 550                   apply le_O_n
 551                 ]
 552               | rewrite < sym_times.
 553                 assumption
 554               ]
 555             ]
 556           | apply lt_mod_m_m.
 557             unfold lt.
 558             apply le_S_S.
 559             apply le_O_n
 560           ]
 561         | unfold lt.
 562           rewrite > S_pred in \vdash (? ? %)
 563           [ apply le_S_S.
 564             assumption
 565           | apply lt_O_times_S_S
 566           ]
 567         ]
 568       | unfold lt.
 569         rewrite > S_pred in \vdash (? ? %)
 570         [ apply le_S_S.
 571           assumption
 572         | apply lt_O_times_S_S
 573         ]
 574       ]
 575     ]
 576   | intros.
 577     apply False_ind.
 578     apply (not_le_Sn_O m1 H4)
 579   ]
 580 | apply lt_O_times_S_S
 581 ]
 582 qed.
 583
 584 theorem sigma_p_knm:
 585 \forall g: nat \to nat.
 586 \forall h2:nat \to nat \to nat.
 587 \forall h11,h12:nat \to nat.
 588 \forall k,n,m.
 589 \forall p1,p21:nat \to bool.
 590 \forall p22:nat \to nat \to bool.
 591 (\forall x. x < k \to p1 x = true \to
 592 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
 593 \land h2 (h11 x) (h12 x) = x
 594 \land (h11 x) < n \land (h12 x) < m) \to
 595 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
 596 p1 (h2 i j) = true \land
 597 h11 (h2 i j) = i \land h12 (h2 i j) = j
 598 \land h2 i j < k) \to
 599 sigma_p k p1 g=
 600 sigma_p n p21 (\lambda x:nat.sigma_p m (p22 x) (\lambda y. g (h2 x y))).
 601 intros.
 602 unfold sigma_p.
 603 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
 604 apply iter_p_gen_knm
 605   [apply symmetricIntPlus
 606   |apply associative_plus
 607   |intro.rewrite < plus_n_O.reflexivity
 608   |exact h11
 609   |exact h12
 610   |assumption
 611   |assumption
 612   ]
 613 qed.
 614