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 (* sigma from n1*m1 to n2*m2 *)
 318 theorem sigma_p2_eq:
 319 \forall g: nat \to nat \to Z.
 320 \forall h11,h12,h21,h22: nat \to nat \to nat.
 321 \forall n1,m1,n2,m2.
 322 \forall p11,p21:nat \to bool.
 323 \forall p12,p22:nat \to nat \to bool.
 324 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
 325 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
 326 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
 327 \land h11 i j < n1 \land h12 i j < m1) \to
 328 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
 329 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
 330 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
 331 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
 332 sigma_p n1 p11 (\lambda x:nat .sigma_p m1 (p12 x) (\lambda y. g x y)) =
 333 sigma_p n2 p21 (\lambda x:nat .sigma_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
 334 intros.
 335 rewrite < sigma_p2'.
 336 rewrite < sigma_p2'.
 337 apply sym_eq.
 338 letin h := (\lambda x.(h11 (x/m2) (x\mod m2))*m1 + (h12 (x/m2) (x\mod m2))).
 339 letin h1 := (\lambda x.(h21 (x/m1) (x\mod m1))*m2 + (h22 (x/m1) (x\mod m1))).
 340 apply (trans_eq ? ?
 341   (sigma_p (n2*m2) (\lambda x:nat.p21 (x/m2)\land p22 (x/m2) (x\mod m2))
 342   (\lambda x:nat.g ((h x)/m1) ((h x)\mod m1))))
 343   [clear h.clear h1.
 344    apply eq_sigma_p1
 345     [intros.reflexivity
 346     |intros.
 347      cut (O < m2)
 348       [cut (x/m2 < n2)
 349         [cut (x \mod m2 < m2)
 350           [elim (and_true ? ? H3).
 351            elim (H ? ? Hcut1 Hcut2 H4 H5).
 352            elim H6.clear H6.
 353            elim H8.clear H8.
 354            elim H6.clear H6.
 355            elim H8.clear H8.
 356            apply eq_f2
 357             [apply sym_eq.
 358              apply div_plus_times.
 359              assumption
 360             |autobatch
 361             ]
 362           |apply lt_mod_m_m.
 363            assumption
 364           ]
 365         |apply (lt_times_n_to_lt m2)
 366           [assumption
 367           |apply (le_to_lt_to_lt ? x)
 368             [apply (eq_plus_to_le ? ? (x \mod m2)).
 369              apply div_mod.
 370              assumption
 371             |assumption
 372             ]
 373           ]
 374         ]
 375       |apply not_le_to_lt.unfold.intro.
 376        generalize in match H2.
 377        apply (le_n_O_elim ? H4).
 378        rewrite < times_n_O.
 379        apply le_to_not_lt.
 380        apply le_O_n
 381       ]
 382     ]
 383   |apply (eq_sigma_p_gh ? h h1);intros
 384     [cut (O < m2)
 385       [cut (i/m2 < n2)
 386         [cut (i \mod m2 < m2)
 387           [elim (and_true ? ? H3).
 388            elim (H ? ? Hcut1 Hcut2 H4 H5).
 389            elim H6.clear H6.
 390            elim H8.clear H8.
 391            elim H6.clear H6.
 392            elim H8.clear H8.
 393            cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 =
 394                  h11 (i/m2) (i\mod m2))
 395             [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
 396                   h12 (i/m2) (i\mod m2))
 397               [rewrite > Hcut3.
 398                rewrite > Hcut4.
 399                rewrite > H6.
 400                rewrite > H12.
 401                reflexivity
 402               |apply mod_plus_times.
 403                assumption
 404               ]
 405             |apply div_plus_times.
 406              assumption
 407             ]
 408           |apply lt_mod_m_m.
 409            assumption
 410           ]
 411         |apply (lt_times_n_to_lt m2)
 412           [assumption
 413           |apply (le_to_lt_to_lt ? i)
 414             [apply (eq_plus_to_le ? ? (i \mod m2)).
 415              apply div_mod.
 416              assumption
 417             |assumption
 418             ]
 419           ]
 420         ]
 421       |apply not_le_to_lt.unfold.intro.
 422        generalize in match H2.
 423        apply (le_n_O_elim ? H4).
 424        rewrite < times_n_O.
 425        apply le_to_not_lt.
 426        apply le_O_n
 427       ]
 428     |cut (O < m2)
 429       [cut (i/m2 < n2)
 430         [cut (i \mod m2 < m2)
 431           [elim (and_true ? ? H3).
 432            elim (H ? ? Hcut1 Hcut2 H4 H5).
 433            elim H6.clear H6.
 434            elim H8.clear H8.
 435            elim H6.clear H6.
 436            elim H8.clear H8.
 437            cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 =
 438                  h11 (i/m2) (i\mod m2))
 439             [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
 440                   h12 (i/m2) (i\mod m2))
 441               [rewrite > Hcut3.
 442                rewrite > Hcut4.
 443                rewrite > H10.
 444                rewrite > H11.
 445                apply sym_eq.
 446                apply div_mod.
 447                assumption
 448               |apply mod_plus_times.
 449                assumption
 450               ]
 451             |apply div_plus_times.
 452              assumption
 453             ]
 454           |apply lt_mod_m_m.
 455            assumption
 456           ]
 457         |apply (lt_times_n_to_lt m2)
 458           [assumption
 459           |apply (le_to_lt_to_lt ? i)
 460             [apply (eq_plus_to_le ? ? (i \mod m2)).
 461              apply div_mod.
 462              assumption
 463             |assumption
 464             ]
 465           ]
 466         ]
 467       |apply not_le_to_lt.unfold.intro.
 468        generalize in match H2.
 469        apply (le_n_O_elim ? H4).
 470        rewrite < times_n_O.
 471        apply le_to_not_lt.
 472        apply le_O_n
 473       ]
 474     |cut (O < m2)
 475       [cut (i/m2 < n2)
 476         [cut (i \mod m2 < m2)
 477           [elim (and_true ? ? H3).
 478            elim (H ? ? Hcut1 Hcut2 H4 H5).
 479            elim H6.clear H6.
 480            elim H8.clear H8.
 481            elim H6.clear H6.
 482            elim H8.clear H8.
 483            apply lt_times_plus_times
 484             [assumption|assumption]
 485           |apply lt_mod_m_m.
 486            assumption
 487           ]
 488         |apply (lt_times_n_to_lt m2)
 489           [assumption
 490           |apply (le_to_lt_to_lt ? i)
 491             [apply (eq_plus_to_le ? ? (i \mod m2)).
 492              apply div_mod.
 493              assumption
 494             |assumption
 495             ]
 496           ]
 497         ]
 498       |apply not_le_to_lt.unfold.intro.
 499        generalize in match H2.
 500        apply (le_n_O_elim ? H4).
 501        rewrite < times_n_O.
 502        apply le_to_not_lt.
 503        apply le_O_n
 504       ]
 505     |cut (O < m1)
 506       [cut (j/m1 < n1)
 507         [cut (j \mod m1 < m1)
 508           [elim (and_true ? ? H3).
 509            elim (H1 ? ? Hcut1 Hcut2 H4 H5).
 510            elim H6.clear H6.
 511            elim H8.clear H8.
 512            elim H6.clear H6.
 513            elim H8.clear H8.
 514            cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 =
 515                  h21 (j/m1) (j\mod m1))
 516             [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
 517                   h22 (j/m1) (j\mod m1))
 518               [rewrite > Hcut3.
 519                rewrite > Hcut4.
 520                rewrite > H6.
 521                rewrite > H12.
 522                reflexivity
 523               |apply mod_plus_times.
 524                assumption
 525               ]
 526             |apply div_plus_times.
 527              assumption
 528             ]
 529           |apply lt_mod_m_m.
 530            assumption
 531           ]
 532         |apply (lt_times_n_to_lt m1)
 533           [assumption
 534           |apply (le_to_lt_to_lt ? j)
 535             [apply (eq_plus_to_le ? ? (j \mod m1)).
 536              apply div_mod.
 537              assumption
 538             |assumption
 539             ]
 540           ]
 541         ]
 542       |apply not_le_to_lt.unfold.intro.
 543        generalize in match H2.
 544        apply (le_n_O_elim ? H4).
 545        rewrite < times_n_O.
 546        apply le_to_not_lt.
 547        apply le_O_n
 548       ]
 549     |cut (O < m1)
 550       [cut (j/m1 < n1)
 551         [cut (j \mod m1 < m1)
 552           [elim (and_true ? ? H3).
 553            elim (H1 ? ? Hcut1 Hcut2 H4 H5).
 554            elim H6.clear H6.
 555            elim H8.clear H8.
 556            elim H6.clear H6.
 557            elim H8.clear H8.
 558            cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 =
 559                  h21 (j/m1) (j\mod m1))
 560             [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
 561                   h22 (j/m1) (j\mod m1))
 562               [rewrite > Hcut3.
 563                rewrite > Hcut4.
 564                rewrite > H10.
 565                rewrite > H11.
 566                apply sym_eq.
 567                apply div_mod.
 568                assumption
 569               |apply mod_plus_times.
 570                assumption
 571               ]
 572             |apply div_plus_times.
 573              assumption
 574             ]
 575           |apply lt_mod_m_m.
 576            assumption
 577           ]
 578         |apply (lt_times_n_to_lt m1)
 579           [assumption
 580           |apply (le_to_lt_to_lt ? j)
 581             [apply (eq_plus_to_le ? ? (j \mod m1)).
 582              apply div_mod.
 583              assumption
 584             |assumption
 585             ]
 586           ]
 587         ]
 588       |apply not_le_to_lt.unfold.intro.
 589        generalize in match H2.
 590        apply (le_n_O_elim ? H4).
 591        rewrite < times_n_O.
 592        apply le_to_not_lt.
 593        apply le_O_n
 594       ]
 595     |cut (O < m1)
 596       [cut (j/m1 < n1)
 597         [cut (j \mod m1 < m1)
 598           [elim (and_true ? ? H3).
 599            elim (H1 ? ? Hcut1 Hcut2 H4 H5).
 600            elim H6.clear H6.
 601            elim H8.clear H8.
 602            elim H6.clear H6.
 603            elim H8.clear H8.
 604            apply (lt_times_plus_times ? ? ? m2)
 605             [assumption|assumption]
 606           |apply lt_mod_m_m.
 607            assumption
 608           ]
 609         |apply (lt_times_n_to_lt m1)
 610           [assumption
 611           |apply (le_to_lt_to_lt ? j)
 612             [apply (eq_plus_to_le ? ? (j \mod m1)).
 613              apply div_mod.
 614              assumption
 615             |assumption
 616             ]
 617           ]
 618         ]
 619       |apply not_le_to_lt.unfold.intro.
 620        generalize in match H2.
 621        apply (le_n_O_elim ? H4).
 622        rewrite < times_n_O.
 623        apply le_to_not_lt.
 624        apply le_O_n
 625       ]
 626     ]
 627   ]
 628 qed.