helm/software/matita/library/Z/sigma_p.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 include "Z/times.ma".
  16 include "nat/primes.ma".
  17 include "nat/ord.ma".
  18 include "nat/generic_iter_p.ma".
  19
  20 (* sigma_p in Z is a specialization of iter_p_gen *)
  21 definition sigma_p: nat \to (nat \to bool) \to (nat \to Z) \to Z \def
  22 \lambda n, p, g. (iter_p_gen n p Z g OZ Zplus).
  23
  24 theorem symmetricZPlus: symmetric Z Zplus.
  25 change with (\forall a,b:Z. (Zplus a b) = (Zplus b a)).
  26 intros.
  27 rewrite > sym_Zplus.
  28 reflexivity.
  29 qed.
  30
  31 theorem true_to_sigma_p_Sn:
  32 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to Z.
  33 p n = true \to sigma_p (S n) p g =
  34 (g n)+(sigma_p n p g).
  35 intros.
  36 unfold sigma_p.
  37 apply true_to_iter_p_gen_Sn.
  38 assumption.
  39 qed.
  40
  41 theorem false_to_sigma_p_Sn:
  42 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to Z.
  43 p n = false \to sigma_p (S n) p g = sigma_p n p g.
  44 intros.
  45 unfold sigma_p.
  46 apply false_to_iter_p_gen_Sn.
  47 assumption.
  48 qed.
  49
  50 theorem eq_sigma_p: \forall p1,p2:nat \to bool.
  51 \forall g1,g2: nat \to Z.\forall n.
  52 (\forall x.  x < n \to p1 x = p2 x) \to
  53 (\forall x.  x < n \to g1 x = g2 x) \to
  54 sigma_p n p1 g1 = sigma_p n p2 g2.
  55 intros.
  56 unfold sigma_p.
  57 apply eq_iter_p_gen;
  58   assumption.
  59 qed.
  60
  61 theorem eq_sigma_p1: \forall p1,p2:nat \to bool.
  62 \forall g1,g2: nat \to Z.\forall n.
  63 (\forall x.  x < n \to p1 x = p2 x) \to
  64 (\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
  65 sigma_p n p1 g1 = sigma_p n p2 g2.
  66 intros.
  67 unfold sigma_p.
  68 apply eq_iter_p_gen1;
  69   assumption.
  70 qed.
  71
  72 theorem sigma_p_false:
  73 \forall g: nat \to Z.\forall n.sigma_p n (\lambda x.false) g = O.
  74 intros.
  75 unfold sigma_p.
  76 apply iter_p_gen_false.
  77 qed.
  78
  79 theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
  80 \forall g: nat \to Z.
  81 sigma_p (k+n) p g
  82 = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
  83 intros.
  84 unfold sigma_p.
  85 apply (iter_p_gen_plusA Z n k p g OZ Zplus)
  86 [ apply symmetricZPlus.
  87 | intros.
  88   apply Zplus_z_OZ.
  89 | apply associative_Zplus
  90 ]
  91 qed.
  92
  93 theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to
  94 \forall p:nat \to bool.
  95 \forall g: nat \to Z. (\forall i:nat. n \le i \to i < m \to
  96 p i = false) \to sigma_p m p g = sigma_p n p g.
  97 intros.
  98 unfold sigma_p.
  99 apply (false_to_eq_iter_p_gen);
 100   assumption.
 101 qed.
 102
 103 theorem sigma_p2 :
 104 \forall n,m:nat.
 105 \forall p1,p2:nat \to bool.
 106 \forall g: nat \to nat \to Z.
 107 sigma_p (n*m)
 108   (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
 109   (\lambda x.g (div x m) (mod x m)) =
 110 sigma_p n p1
 111   (\lambda x.sigma_p m p2 (g x)).
 112 intros.
 113 unfold sigma_p.
 114 apply (iter_p_gen2 n m p1 p2 Z g OZ Zplus)
 115 [ apply symmetricZPlus
 116 | apply associative_Zplus
 117 | intros.
 118   apply Zplus_z_OZ
 119 ]
 120 qed.
 121
 122 (* a stronger, dependent version, required e.g. for dirichlet product *)
 123
 124 theorem sigma_p2' :
 125 \forall n,m:nat.
 126 \forall p1:nat \to bool.
 127 \forall p2:nat \to nat \to bool.
 128 \forall g: nat \to nat \to Z.
 129 sigma_p (n*m)
 130   (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m)))
 131   (\lambda x.g (div x m) (mod x m)) =
 132 sigma_p n p1
 133   (\lambda x.sigma_p m (p2 x) (g x)).
 134 intros.
 135 unfold sigma_p.
 136 apply (iter_p_gen2' n m p1 p2 Z g OZ Zplus)
 137 [ apply symmetricZPlus
 138 | apply associative_Zplus
 139 | intros.
 140   apply Zplus_z_OZ
 141 ]
 142 qed.
 143
 144 lemma sigma_p_gi: \forall g: nat \to Z.
 145 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
 146 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
 147 intros.
 148 unfold sigma_p.
 149 apply (iter_p_gen_gi)
 150 [ apply symmetricZPlus
 151 | apply associative_Zplus
 152 | intros.
 153   apply Zplus_z_OZ
 154 | assumption
 155 | assumption
 156 ]
 157 qed.
 158
 159 theorem eq_sigma_p_gh:
 160 \forall g: nat \to Z.
 161 \forall h,h1: nat \to nat.\forall n,n1.
 162 \forall p1,p2:nat \to bool.
 163 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
 164 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
 165 (\forall i. i < n \to p1 i = true \to h i < n1) \to
 166 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
 167 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
 168 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
 169 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 p2 g.
 170 intros.
 171 unfold sigma_p.
 172 apply (eq_iter_p_gen_gh Z OZ Zplus ? ? ? g h h1 n n1 p1 p2)
 173 [ apply symmetricZPlus
 174 | apply associative_Zplus
 175 | intros.
 176   apply Zplus_z_OZ
 177 | assumption
 178 | assumption
 179 | assumption
 180 | assumption
 181 | assumption
 182 | assumption
 183 ]
 184 qed.
 185
 186
 187 theorem divides_exp_to_lt_ord:\forall n,m,j,p. O < n \to prime p \to
 188 p \ndivides n \to j \divides n*(exp p m) \to ord j p < S m.
 189 intros.
 190 cut (m = ord (n*(exp p m)) p)
 191   [apply le_S_S.
 192    rewrite > Hcut.
 193    apply divides_to_le_ord
 194     [elim (le_to_or_lt_eq ? ? (le_O_n j))
 195       [assumption
 196       |apply False_ind.
 197        apply (lt_to_not_eq ? ? H).
 198        elim H3.
 199        rewrite < H4 in H5.simplify in H5.
 200        elim (times_O_to_O ? ? H5)
 201         [apply sym_eq.assumption
 202         |apply False_ind.
 203          apply (not_le_Sn_n O).
 204          rewrite < H6 in \vdash (? ? %).
 205          apply lt_O_exp.
 206          elim H1.apply lt_to_le.assumption
 207         ]
 208       ]
 209     |rewrite > (times_n_O O).
 210      apply lt_times
 211       [assumption|apply lt_O_exp.apply (prime_to_lt_O ? H1)]
 212     |assumption
 213     |assumption
 214     ]
 215   |unfold ord.
 216    rewrite > (p_ord_exp1 p ? m n)
 217     [reflexivity
 218     |apply (prime_to_lt_O ? H1)
 219     |assumption
 220     |apply sym_times
 221     ]
 222   ]
 223 qed.
 224
 225 theorem divides_exp_to_divides_ord_rem:\forall n,m,j,p. O < n \to prime p \to
 226 p \ndivides n \to j \divides n*(exp p m) \to ord_rem j p \divides n.
 227 intros.
 228 cut (O < j)
 229   [cut (n = ord_rem (n*(exp p m)) p)
 230     [rewrite > Hcut1.
 231      apply divides_to_divides_ord_rem
 232       [assumption
 233       |rewrite > (times_n_O O).
 234        apply lt_times
 235         [assumption|apply lt_O_exp.apply (prime_to_lt_O ? H1)]
 236       |assumption
 237       |assumption
 238       ]
 239     |unfold ord_rem.
 240      rewrite > (p_ord_exp1 p ? m n)
 241       [reflexivity
 242       |apply (prime_to_lt_O ? H1)
 243       |assumption
 244       |apply sym_times
 245       ]
 246     ]
 247   |elim (le_to_or_lt_eq ? ? (le_O_n j))
 248     [assumption
 249     |apply False_ind.
 250      apply (lt_to_not_eq ? ? H).
 251      elim H3.
 252      rewrite < H4 in H5.simplify in H5.
 253      elim (times_O_to_O ? ? H5)
 254       [apply sym_eq.assumption
 255       |apply False_ind.
 256        apply (not_le_Sn_n O).
 257        rewrite < H6 in \vdash (? ? %).
 258        apply lt_O_exp.
 259        elim H1.apply lt_to_le.assumption
 260       ]
 261     ]
 262   ]
 263 qed.
 264
 265
 266 theorem sigma_p_divides_b:
 267 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
 268 \forall g: nat \to Z.
 269 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
 270 sigma_p (S n) (\lambda x.divides_b x n)
 271   (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
 272 intros.
 273 unfold sigma_p.
 274 apply (iter_p_gen_divides Z OZ Zplus n m p ? ? ? g)
 275 [ assumption
 276 | assumption
 277 | assumption
 278 | apply symmetricZPlus
 279 | apply associative_Zplus
 280 | intros.
 281   apply Zplus_z_OZ
 282 ]
 283 qed.
 284
 285
 286 (* sigma_p and Ztimes *)
 287 lemma Ztimes_sigma_pl: \forall z:Z.\forall n:nat.\forall p. \forall f.
 288 z * (sigma_p n p f) = sigma_p n p (\lambda i.z*(f i)).
 289 intros.
 290 apply (distributive_times_plus_iter_p_gen Z Zplus OZ Ztimes n z p f)
 291 [ apply symmetricZPlus
 292 | apply associative_Zplus
 293 | intros.
 294   apply Zplus_z_OZ
 295 | apply symmetric_Ztimes
 296 | apply distributive_Ztimes_Zplus
 297 | intros.
 298   rewrite > (Ztimes_z_OZ a).
 299   reflexivity
 300 ]
 301 qed.
 302
 303 lemma Ztimes_sigma_pr: \forall z:Z.\forall n:nat.\forall p. \forall f.
 304 (sigma_p n p f) * z = sigma_p n p (\lambda i.(f i)*z).
 305 intros.
 306 rewrite < sym_Ztimes.
 307 rewrite > Ztimes_sigma_pl.
 308 apply eq_sigma_p
 309   [intros.reflexivity
 310   |intros.apply sym_Ztimes
 311   ]
 312 qed.
 313
 314
 315 theorem sigma_p_knm:
 316 \forall g: nat \to Z.
 317 \forall h2:nat \to nat \to nat.
 318 \forall h11,h12:nat \to nat.
 319 \forall k,n,m.
 320 \forall p1,p21:nat \to bool.
 321 \forall p22:nat \to nat \to bool.
 322 (\forall x. x < k \to p1 x = true \to
 323 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
 324 \land h2 (h11 x) (h12 x) = x
 325 \land (h11 x) < n \land (h12 x) < m) \to
 326 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
 327 p1 (h2 i j) = true \land
 328 h11 (h2 i j) = i \land h12 (h2 i j) = j
 329 \land h2 i j < k) \to
 330 sigma_p k p1 g=
 331 sigma_p n p21 (\lambda x:nat.sigma_p m (p22 x) (\lambda y. g (h2 x y))).
 332 intros.
 333 unfold sigma_p.
 334 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
 335 apply iter_p_gen_knm
 336   [ apply symmetricZPlus
 337   |apply associative_Zplus
 338   | intro.
 339     apply (Zplus_z_OZ a)
 340   | exact h11
 341   | exact h12
 342   | assumption
 343   | assumption
 344   ]
 345 qed.
 346
 347
 348 theorem sigma_p2_eq:
 349 \forall g: nat \to nat \to Z.
 350 \forall h11,h12,h21,h22: nat \to nat \to nat.
 351 \forall n1,m1,n2,m2.
 352 \forall p11,p21:nat \to bool.
 353 \forall p12,p22:nat \to nat \to bool.
 354 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
 355 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
 356 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
 357 \land h11 i j < n1 \land h12 i j < m1) \to
 358 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
 359 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
 360 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
 361 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
 362 sigma_p n1 p11 (\lambda x:nat .sigma_p m1 (p12 x) (\lambda y. g x y)) =
 363 sigma_p n2 p21 (\lambda x:nat .sigma_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
 364 intros.
 365 unfold sigma_p.
 366 unfold sigma_p in \vdash (? ? (? ? ? ? (\lambda x:?.%) ? ?) ?).
 367 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
 368
 369 apply(iter_p_gen_2_eq Z OZ Zplus ? ? ? g h11 h12 h21 h22 n1 m1 n2 m2 p11 p21 p12 p22)
 370 [ apply symmetricZPlus
 371 | apply associative_Zplus
 372 | intro.
 373   apply (Zplus_z_OZ a)
 374 | assumption
 375 | assumption
 376 ]
 377 qed.
 378
 379
 380
 381
 382 (*
 383
 384
 385
 386
 387
 388 rewrite < sigma_p2'.
 389 letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))).
 390 letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))).
 391 letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))).
 392
 393 apply (trans_eq ? ?
 394 (sigma_p n2 p21 (\lambda x:nat. sigma_p m2 (p22 x)
 395  (\lambda y:nat.(g (((h11 x y)*m1+(h12 x y))/m1) (((h11 x y)*m1+(h12 x y))\mod m1)) ) ) ))
 396 [
 397   apply (sigma_p_knm (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros
 398   [ elim (and_true ? ? H3).
 399     cut(O \lt m1)
 400     [ cut(x/m1 < n1)
 401       [ cut((x \mod m1) < m1)
 402         [ elim (H1 ? ? Hcut1 Hcut2 H4 H5).
 403           elim H6.clear H6.
 404           elim H8.clear H8.
 405           elim H6.clear H6.
 406           elim H8.clear H8.
 407           split
 408           [ split
 409             [ split
 410               [ split
 411                 [ assumption
 412                 | assumption
 413                 ]
 414               | rewrite > H11.
 415                 rewrite > H10.
 416                 apply sym_eq.
 417                 apply div_mod.
 418                 assumption
 419               ]
 420             | assumption
 421             ]
 422           | assumption
 423           ]
 424         | apply lt_mod_m_m.
 425           assumption
 426         ]
 427       | apply (lt_times_n_to_lt m1)
 428         [ assumption
 429         | apply (le_to_lt_to_lt ? x)
 430           [ apply (eq_plus_to_le ? ? (x \mod m1)).
 431             apply div_mod.
 432             assumption
 433           | assumption
 434         ]
 435       ]
 436     ]
 437     | apply not_le_to_lt.unfold.intro.
 438       generalize in match H2.
 439       apply (le_n_O_elim ? H6).
 440       rewrite < times_n_O.
 441       apply le_to_not_lt.
 442       apply le_O_n.
 443     ]
 444   | elim (H ? ? H2 H3 H4 H5).
 445     elim H6.clear H6.
 446     elim H8.clear H8.
 447     elim H6.clear H6.
 448     elim H8.clear H8.
 449     cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j))
 450     [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j))
 451       [ split
 452         [ split
 453           [ split
 454             [ apply true_to_true_to_andb_true
 455               [ rewrite > Hcut.
 456                 assumption
 457               | rewrite > Hcut1.
 458                 rewrite > Hcut.
 459                 assumption
 460               ]
 461             | rewrite > Hcut1.
 462               rewrite > Hcut.
 463               assumption
 464             ]
 465           | rewrite > Hcut1.
 466             rewrite > Hcut.
 467             assumption
 468           ]
 469         | cut(O \lt m1)
 470           [ cut(O \lt n1)
 471             [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
 472               [ apply (lt_plus_r).
 473                 assumption
 474               | rewrite > sym_plus.
 475                 rewrite > (sym_times (h11 i j) m1).
 476                 rewrite > times_n_Sm.
 477                 rewrite > sym_times.
 478                 apply (le_times_l).
 479                 assumption
 480               ]
 481             | apply not_le_to_lt.unfold.intro.
 482               generalize in match H9.
 483               apply (le_n_O_elim ? H8).
 484               apply le_to_not_lt.
 485               apply le_O_n
 486             ]
 487           | apply not_le_to_lt.unfold.intro.
 488             generalize in match H7.
 489             apply (le_n_O_elim ? H8).
 490             apply le_to_not_lt.
 491             apply le_O_n
 492           ]
 493         ]
 494       | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)).
 495         reflexivity.
 496         assumption
 497       ]
 498     | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)).
 499       reflexivity.
 500       assumption
 501     ]
 502   ]
 503 | apply (eq_sigma_p1)
 504   [ intros. reflexivity
 505   | intros.
 506     apply (eq_sigma_p1)
 507     [ intros. reflexivity
 508     | intros.
 509       rewrite > (div_plus_times)
 510       [ rewrite > (mod_plus_times)
 511         [ reflexivity
 512         | elim (H x x1 H2 H4 H3 H5).
 513           assumption
 514         ]
 515       | elim (H x x1 H2 H4 H3 H5).
 516         assumption
 517       ]
 518     ]
 519   ]
 520 ]
 521 qed.
 522
 523 rewrite < sigma_p2' in \vdash (? ? ? %).
 524 apply sym_eq.
 525 letin h := (\lambda x.(h11 (x/m2) (x\mod m2))*m1 + (h12 (x/m2) (x\mod m2))).
 526 letin h1 := (\lambda x.(h21 (x/m1) (x\mod m1))*m2 + (h22 (x/m1) (x\mod m1))).
 527 apply (trans_eq ? ?
 528   (sigma_p (n2*m2) (\lambda x:nat.p21 (x/m2)\land p22 (x/m2) (x\mod m2))
 529   (\lambda x:nat.g ((h x)/m1) ((h x)\mod m1))))
 530   [clear h.clear h1.
 531    apply eq_sigma_p1
 532     [intros.reflexivity
 533     |intros.
 534      cut (O < m2)
 535       [cut (x/m2 < n2)
 536         [cut (x \mod m2 < m2)
 537           [elim (and_true ? ? H3).
 538            elim (H ? ? Hcut1 Hcut2 H4 H5).
 539            elim H6.clear H6.
 540            elim H8.clear H8.
 541            elim H6.clear H6.
 542            elim H8.clear H8.
 543            apply eq_f2
 544             [apply sym_eq.
 545              apply div_plus_times.
 546              assumption
 547             |
 548               apply sym_eq.
 549               apply mod_plus_times.
 550               assumption
 551             ]
 552           |apply lt_mod_m_m.
 553            assumption
 554           ]
 555         |apply (lt_times_n_to_lt m2)
 556           [assumption
 557           |apply (le_to_lt_to_lt ? x)
 558             [apply (eq_plus_to_le ? ? (x \mod m2)).
 559              apply div_mod.
 560              assumption
 561             |assumption
 562             ]
 563           ]
 564         ]
 565       |apply not_le_to_lt.unfold.intro.
 566        generalize in match H2.
 567        apply (le_n_O_elim ? H4).
 568        rewrite < times_n_O.
 569        apply le_to_not_lt.
 570        apply le_O_n
 571       ]
 572     ]
 573   |apply (eq_sigma_p_gh ? h h1);intros
 574     [cut (O < m2)
 575       [cut (i/m2 < n2)
 576         [cut (i \mod m2 < m2)
 577           [elim (and_true ? ? H3).
 578            elim (H ? ? Hcut1 Hcut2 H4 H5).
 579            elim H6.clear H6.
 580            elim H8.clear H8.
 581            elim H6.clear H6.
 582            elim H8.clear H8.
 583            cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 =
 584                  h11 (i/m2) (i\mod m2))
 585             [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
 586                   h12 (i/m2) (i\mod m2))
 587               [rewrite > Hcut3.
 588                rewrite > Hcut4.
 589                rewrite > H6.
 590                rewrite > H12.
 591                reflexivity
 592               |apply mod_plus_times.
 593                assumption
 594               ]
 595             |apply div_plus_times.
 596              assumption
 597             ]
 598           |apply lt_mod_m_m.
 599            assumption
 600           ]
 601         |apply (lt_times_n_to_lt m2)
 602           [assumption
 603           |apply (le_to_lt_to_lt ? i)
 604             [apply (eq_plus_to_le ? ? (i \mod m2)).
 605              apply div_mod.
 606              assumption
 607             |assumption
 608             ]
 609           ]
 610         ]
 611       |apply not_le_to_lt.unfold.intro.
 612        generalize in match H2.
 613        apply (le_n_O_elim ? H4).
 614        rewrite < times_n_O.
 615        apply le_to_not_lt.
 616        apply le_O_n
 617       ]
 618     |cut (O < m2)
 619       [cut (i/m2 < n2)
 620         [cut (i \mod m2 < m2)
 621           [elim (and_true ? ? H3).
 622            elim (H ? ? Hcut1 Hcut2 H4 H5).
 623            elim H6.clear H6.
 624            elim H8.clear H8.
 625            elim H6.clear H6.
 626            elim H8.clear H8.
 627            cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 =
 628                  h11 (i/m2) (i\mod m2))
 629             [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
 630                   h12 (i/m2) (i\mod m2))
 631               [rewrite > Hcut3.
 632                rewrite > Hcut4.
 633                rewrite > H10.
 634                rewrite > H11.
 635                apply sym_eq.
 636                apply div_mod.
 637                assumption
 638               |apply mod_plus_times.
 639                assumption
 640               ]
 641             |apply div_plus_times.
 642              assumption
 643             ]
 644           |apply lt_mod_m_m.
 645            assumption
 646           ]
 647         |apply (lt_times_n_to_lt m2)
 648           [assumption
 649           |apply (le_to_lt_to_lt ? i)
 650             [apply (eq_plus_to_le ? ? (i \mod m2)).
 651              apply div_mod.
 652              assumption
 653             |assumption
 654             ]
 655           ]
 656         ]
 657       |apply not_le_to_lt.unfold.intro.
 658        generalize in match H2.
 659        apply (le_n_O_elim ? H4).
 660        rewrite < times_n_O.
 661        apply le_to_not_lt.
 662        apply le_O_n
 663       ]
 664     |cut (O < m2)
 665       [cut (i/m2 < n2)
 666         [cut (i \mod m2 < m2)
 667           [elim (and_true ? ? H3).
 668            elim (H ? ? Hcut1 Hcut2 H4 H5).
 669            elim H6.clear H6.
 670            elim H8.clear H8.
 671            elim H6.clear H6.
 672            elim H8.clear H8.
 673            apply lt_times_plus_times
 674             [assumption|assumption]
 675           |apply lt_mod_m_m.
 676            assumption
 677           ]
 678         |apply (lt_times_n_to_lt m2)
 679           [assumption
 680           |apply (le_to_lt_to_lt ? i)
 681             [apply (eq_plus_to_le ? ? (i \mod m2)).
 682              apply div_mod.
 683              assumption
 684             |assumption
 685             ]
 686           ]
 687         ]
 688       |apply not_le_to_lt.unfold.intro.
 689        generalize in match H2.
 690        apply (le_n_O_elim ? H4).
 691        rewrite < times_n_O.
 692        apply le_to_not_lt.
 693        apply le_O_n
 694       ]
 695     |cut (O < m1)
 696       [cut (j/m1 < n1)
 697         [cut (j \mod m1 < m1)
 698           [elim (and_true ? ? H3).
 699            elim (H1 ? ? Hcut1 Hcut2 H4 H5).
 700            elim H6.clear H6.
 701            elim H8.clear H8.
 702            elim H6.clear H6.
 703            elim H8.clear H8.
 704            cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 =
 705                  h21 (j/m1) (j\mod m1))
 706             [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
 707                   h22 (j/m1) (j\mod m1))
 708               [rewrite > Hcut3.
 709                rewrite > Hcut4.
 710                rewrite > H6.
 711                rewrite > H12.
 712                reflexivity
 713               |apply mod_plus_times.
 714                assumption
 715               ]
 716             |apply div_plus_times.
 717              assumption
 718             ]
 719           |apply lt_mod_m_m.
 720            assumption
 721           ]
 722         |apply (lt_times_n_to_lt m1)
 723           [assumption
 724           |apply (le_to_lt_to_lt ? j)
 725             [apply (eq_plus_to_le ? ? (j \mod m1)).
 726              apply div_mod.
 727              assumption
 728             |assumption
 729             ]
 730           ]
 731         ]
 732       |apply not_le_to_lt.unfold.intro.
 733        generalize in match H2.
 734        apply (le_n_O_elim ? H4).
 735        rewrite < times_n_O.
 736        apply le_to_not_lt.
 737        apply le_O_n
 738       ]
 739     |cut (O < m1)
 740       [cut (j/m1 < n1)
 741         [cut (j \mod m1 < m1)
 742           [elim (and_true ? ? H3).
 743            elim (H1 ? ? Hcut1 Hcut2 H4 H5).
 744            elim H6.clear H6.
 745            elim H8.clear H8.
 746            elim H6.clear H6.
 747            elim H8.clear H8.
 748            cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 =
 749                  h21 (j/m1) (j\mod m1))
 750             [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
 751                   h22 (j/m1) (j\mod m1))
 752               [rewrite > Hcut3.
 753                rewrite > Hcut4.
 754                rewrite > H10.
 755                rewrite > H11.
 756                apply sym_eq.
 757                apply div_mod.
 758                assumption
 759               |apply mod_plus_times.
 760                assumption
 761               ]
 762             |apply div_plus_times.
 763              assumption
 764             ]
 765           |apply lt_mod_m_m.
 766            assumption
 767           ]
 768         |apply (lt_times_n_to_lt m1)
 769           [assumption
 770           |apply (le_to_lt_to_lt ? j)
 771             [apply (eq_plus_to_le ? ? (j \mod m1)).
 772              apply div_mod.
 773              assumption
 774             |assumption
 775             ]
 776           ]
 777         ]
 778       |apply not_le_to_lt.unfold.intro.
 779        generalize in match H2.
 780        apply (le_n_O_elim ? H4).
 781        rewrite < times_n_O.
 782        apply le_to_not_lt.
 783        apply le_O_n
 784       ]
 785     |cut (O < m1)
 786       [cut (j/m1 < n1)
 787         [cut (j \mod m1 < m1)
 788           [elim (and_true ? ? H3).
 789            elim (H1 ? ? Hcut1 Hcut2 H4 H5).
 790            elim H6.clear H6.
 791            elim H8.clear H8.
 792            elim H6.clear H6.
 793            elim H8.clear H8.
 794            apply (lt_times_plus_times ? ? ? m2)
 795             [assumption|assumption]
 796           |apply lt_mod_m_m.
 797            assumption
 798           ]
 799         |apply (lt_times_n_to_lt m1)
 800           [assumption
 801           |apply (le_to_lt_to_lt ? j)
 802             [apply (eq_plus_to_le ? ? (j \mod m1)).
 803              apply div_mod.
 804              assumption
 805             |assumption
 806             ]
 807           ]
 808         ]
 809       |apply not_le_to_lt.unfold.intro.
 810        generalize in match H2.
 811        apply (le_n_O_elim ? H4).
 812        rewrite < times_n_O.
 813        apply le_to_not_lt.
 814        apply le_O_n
 815       ]
 816     ]
 817   ]
 818 qed.
 819 *)
 820
 821