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