matita/library/nat/ord.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 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "datatypes/constructors.ma".
  18 include "nat/exp.ma".
  19 include "nat/nth_prime.ma".
  20 include "nat/gcd.ma". (* for some properties of divides *)
  21 include "nat/relevant_equations.ma". (* required by autobatch paramod *)
  22
  23 let rec p_ord_aux p n m \def
  24   match n \mod m with
  25   [ O \Rightarrow
  26     match p with
  27       [ O \Rightarrow pair nat nat O n
  28       | (S p) \Rightarrow
  29        match (p_ord_aux p (n / m) m) with
  30        [ (pair q r) \Rightarrow pair nat nat (S q) r] ]
  31   | (S a) \Rightarrow pair nat nat O n].
  32
  33 (* p_ord n m = <q,r> if m divides n q times, with remainder r *)
  34 definition p_ord \def \lambda n,m:nat.p_ord_aux n n m.
  35
  36 theorem p_ord_aux_to_Prop: \forall p,n,m. O < m \to
  37   match p_ord_aux p n m with
  38   [ (pair q r) \Rightarrow n = m \sup q *r ].
  39 intro.
  40 elim p.simplify.
  41 apply (nat_case (n \mod m)).
  42 simplify.apply plus_n_O.
  43 intros.
  44 simplify.apply plus_n_O.
  45 simplify.
  46 apply (nat_case1 (n1 \mod m)).intro.
  47 simplify.
  48 generalize in match (H (n1 / m) m).
  49 elim (p_ord_aux n (n1 / m) m).
  50 simplify.
  51 rewrite > assoc_times.
  52 rewrite < H3.rewrite > (plus_n_O (m*(n1 / m))).
  53 rewrite < H2.
  54 rewrite > sym_times.
  55 rewrite < div_mod.reflexivity.
  56 assumption.assumption.
  57 intros.simplify.apply plus_n_O.
  58 qed.
  59
  60 theorem p_ord_aux_to_exp: \forall p,n,m,q,r. O < m \to
  61   (pair nat nat q r) = p_ord_aux p n m \to n = m \sup q * r.
  62 intros.
  63 change with
  64 match (pair nat nat q r) with
  65   [ (pair q r) \Rightarrow n = m \sup q * r ].
  66 rewrite > H1.
  67 apply p_ord_aux_to_Prop.
  68 assumption.
  69 qed.
  70
  71 (* questo va spostato in primes1.ma *)
  72 theorem p_ord_exp: \forall n,m,i. O < m \to n \mod m \neq O \to
  73 \forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n.
  74 intros 5.
  75 elim i.
  76 simplify.
  77 rewrite < plus_n_O.
  78 apply (nat_case p).
  79 simplify.
  80 elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
  81 intro.
  82 simplify.
  83 cut (O < n \mod m \lor O = n \mod m).
  84 elim Hcut.apply (lt_O_n_elim (n \mod m) H3).
  85 intros. simplify.reflexivity.
  86 apply False_ind.
  87 apply H1.apply sym_eq.assumption.
  88 apply le_to_or_lt_eq.apply le_O_n.
  89 generalize in match H3.
  90 apply (nat_case p).intro.apply False_ind.apply (not_le_Sn_O n1 H4).
  91 intros.
  92 simplify. fold simplify (m \sup (S n1)).
  93 cut (((m \sup (S n1)*n) \mod m) = O).
  94 rewrite > Hcut.
  95 simplify.fold simplify (m \sup (S n1)).
  96 cut ((m \sup (S n1) *n) / m = m \sup n1 *n).
  97 rewrite > Hcut1.
  98 rewrite > (H2 m1). simplify.reflexivity.
  99 apply le_S_S_to_le.assumption.
 100 (* div_exp *)
 101 simplify.
 102 rewrite > assoc_times.
 103 apply (lt_O_n_elim m H).
 104 intro.apply div_times.
 105 (* mod_exp = O *)
 106 apply divides_to_mod_O.
 107 assumption.
 108 simplify.rewrite > assoc_times.
 109 apply (witness ? ? (m \sup n1 *n)).reflexivity.
 110 qed.
 111
 112 theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
 113   match p_ord_aux p n m with
 114   [ (pair q r) \Rightarrow r \mod m \neq O].
 115 intro.elim p.absurd (O < n).assumption.
 116 apply le_to_not_lt.assumption.
 117 simplify.
 118 apply (nat_case1 (n1 \mod m)).intro.
 119 generalize in match (H (n1 / m) m).
 120 elim (p_ord_aux n (n1 / m) m).
 121 apply H5.assumption.
 122 apply eq_mod_O_to_lt_O_div.
 123 apply (trans_lt ? (S O)).unfold lt.apply le_n.
 124 assumption.assumption.assumption.
 125 apply le_S_S_to_le.
 126 apply (trans_le ? n1).change with (n1 / m < n1).
 127 apply lt_div_n_m_n.assumption.assumption.assumption.
 128 intros.simplify.
 129 rewrite > H4.
 130 unfold Not.intro.
 131 apply (not_eq_O_S m1).
 132 rewrite > H5.reflexivity.
 133 qed.
 134
 135 theorem p_ord_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to
 136  pair nat nat q r = p_ord_aux p n m \to r \mod m \neq O.
 137 intros.
 138 change with
 139   match (pair nat nat q r) with
 140   [ (pair q r) \Rightarrow r \mod m \neq O].
 141 rewrite > H3.
 142 apply p_ord_aux_to_Prop1.
 143 assumption.assumption.assumption.
 144 qed.
 145
 146 theorem p_ord_exp1: \forall p,n,q,r. O < p \to \lnot p \divides r \to
 147 n = p \sup q * r \to p_ord n p = pair nat nat q r.
 148 intros.unfold p_ord.
 149 rewrite > H2.
 150 apply p_ord_exp
 151  [assumption
 152  |unfold.intro.apply H1.
 153   apply mod_O_to_divides[assumption|assumption]
 154  |apply (trans_le ? (p \sup q)).
 155   cut ((S O) \lt p).
 156   elim q.simplify.apply le_n_Sn.
 157   simplify.
 158   generalize in match H3.
 159   apply (nat_case n1).simplify.
 160   rewrite < times_n_SO.intro.assumption.
 161   intros.
 162   apply (trans_le ? (p*(S m))).
 163   apply (trans_le ? ((S (S O))*(S m))).
 164   simplify.rewrite > plus_n_Sm.
 165   rewrite < plus_n_O.
 166   apply le_plus_n.
 167   apply le_times_l.
 168   assumption.
 169   apply le_times_r.assumption.
 170   apply not_eq_to_le_to_lt.
 171   unfold.intro.apply H1.
 172   rewrite < H3.
 173   apply (witness ? r r ?).simplify.apply plus_n_O.
 174   assumption.
 175   rewrite > times_n_SO in \vdash (? % ?).
 176   apply le_times_r.
 177   change with (O \lt r).
 178   apply not_eq_to_le_to_lt.
 179   unfold.intro.
 180   apply H1.rewrite < H3.
 181   apply (witness ? ? O ?).rewrite < times_n_O.reflexivity.
 182   apply le_O_n.
 183   ]
 184 qed.
 185
 186 theorem p_ord_to_exp1: \forall p,n,q,r. (S O) \lt p \to O \lt n \to p_ord n p = pair nat nat q r\to
 187 \lnot p \divides r \land n = p \sup q * r.
 188 intros.
 189 unfold p_ord in H2.
 190 split.unfold.intro.
 191 apply (p_ord_aux_to_not_mod_O n n p q r).assumption.assumption.
 192 apply le_n.symmetry.assumption.
 193 apply divides_to_mod_O.apply (trans_lt ? (S O)).
 194 unfold.apply le_n.assumption.assumption.
 195 apply (p_ord_aux_to_exp n).apply (trans_lt ? (S O)).
 196 unfold.apply le_n.assumption.symmetry.assumption.
 197 qed.
 198
 199 theorem p_ord_times: \forall p,a,b,qa,ra,qb,rb. prime p
 200 \to O \lt a \to O \lt b
 201 \to p_ord a p = pair nat nat qa ra
 202 \to p_ord b p = pair nat nat qb rb
 203 \to p_ord (a*b) p = pair nat nat (qa + qb) (ra*rb).
 204 intros.
 205 cut ((S O) \lt p).
 206 elim (p_ord_to_exp1 ? ? ? ? Hcut H1 H3).
 207 elim (p_ord_to_exp1 ? ? ? ? Hcut H2 H4).
 208 apply p_ord_exp1.
 209 apply (trans_lt ? (S O)).unfold.apply le_n.assumption.
 210 unfold.intro.
 211 elim (divides_times_to_divides ? ? ? H H9).
 212 apply (absurd ? ? H10 H5).
 213 apply (absurd ? ? H10 H7).
 214 (* rewrite > H6.
 215 rewrite > H8. *)
 216 autobatch paramodulation.
 217 unfold prime in H. elim H. assumption.
 218 qed.
 219
 220 theorem fst_p_ord_times: \forall p,a,b. prime p
 221 \to O \lt a \to O \lt b
 222 \to fst ? ? (p_ord (a*b) p) = (fst ? ? (p_ord a p)) + (fst ? ? (p_ord b p)).
 223 intros.
 224 rewrite > (p_ord_times p a b (fst ? ? (p_ord a p)) (snd ? ? (p_ord a p))
 225 (fst ? ? (p_ord b p)) (snd ? ? (p_ord b p)) H H1 H2).
 226 simplify.reflexivity.
 227 apply eq_pair_fst_snd.
 228 apply eq_pair_fst_snd.
 229 qed.
 230
 231 theorem p_ord_p : \forall p:nat. (S O) \lt p \to p_ord p p = pair ? ? (S O) (S O).
 232 intros.
 233 apply p_ord_exp1.
 234 apply (trans_lt ? (S O)). unfold.apply le_n.assumption.
 235 unfold.intro.
 236 apply (absurd ? ? H).
 237 apply le_to_not_lt.
 238 apply divides_to_le.unfold.apply le_n.assumption.
 239 rewrite < times_n_SO.
 240 apply exp_n_SO.
 241 qed.
 242
 243 (* p_ord and divides *)
 244 theorem divides_to_p_ord: \forall p,a,b,c,d,n,m:nat.
 245 O < n \to O < m \to prime p
 246 \to divides n m \to p_ord n p = pair ? ? a b \to
 247 p_ord m p = pair ? ? c d \to divides b d \land a \le c.
 248 intros.
 249 cut (S O < p)
 250   [lapply (p_ord_to_exp1 ? ? ? ? Hcut H H4).
 251    lapply (p_ord_to_exp1 ? ? ? ? Hcut H1 H5).
 252    elim Hletin. clear Hletin.
 253    elim Hletin1. clear Hletin1.
 254    rewrite > H9 in H3.
 255    split
 256     [apply (gcd_SO_to_divides_times_to_divides (exp p c))
 257       [elim (le_to_or_lt_eq ? ? (le_O_n b))
 258         [assumption
 259         |apply False_ind.
 260          apply (lt_to_not_eq O ? H).
 261          rewrite > H7.
 262          rewrite < H10.
 263          autobatch
 264         ]
 265       |elim c
 266         [rewrite > sym_gcd.
 267          apply gcd_SO_n
 268         |simplify.
 269          apply eq_gcd_times_SO
 270           [apply lt_to_le.assumption
 271           |apply lt_O_exp.apply lt_to_le.assumption
 272           |rewrite > sym_gcd.
 273            (* hint non trova prime_to_gcd_SO e
 274               autobatch non chiude il goal *)
 275            apply prime_to_gcd_SO
 276             [assumption|assumption]
 277           |assumption
 278           ]
 279         ]
 280       |apply (trans_divides ? n)
 281         [apply (witness ? ? (exp p a)).
 282          rewrite > sym_times.
 283          assumption
 284         |assumption
 285         ]
 286       ]
 287     |apply (le_exp_to_le p)
 288       [assumption
 289       |apply divides_to_le
 290         [apply lt_O_exp.apply lt_to_le.assumption
 291         |apply (gcd_SO_to_divides_times_to_divides d)
 292           [apply lt_O_exp.apply lt_to_le.assumption
 293           |elim a
 294             [apply gcd_SO_n
 295             |simplify.rewrite < sym_gcd.
 296              apply eq_gcd_times_SO
 297               [apply lt_to_le.assumption
 298               |apply lt_O_exp.apply lt_to_le.assumption
 299               |rewrite > sym_gcd.
 300               (* hint non trova prime_to_gcd_SO e
 301                  autobatch non chiude il goal *)
 302                apply prime_to_gcd_SO
 303                 [assumption|assumption]
 304               |rewrite > sym_gcd. assumption
 305               ]
 306             ]
 307           |apply (trans_divides ? n)
 308             [apply (witness ? ? b).assumption
 309             |rewrite > sym_times.assumption
 310             ]
 311           ]
 312         ]
 313       ]
 314     ]
 315   |elim H2.assumption
 316   ]
 317 qed.
 318
 319 (* p_ord and primes *)
 320 theorem not_divides_to_p_ord_O: \forall n,i.
 321 Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) =
 322 pair nat nat O n.
 323 intros.
 324 apply p_ord_exp1
 325   [apply lt_O_nth_prime_n
 326   |assumption
 327   |autobatch
 328   ]
 329 qed.
 330
 331 theorem p_ord_O_to_not_divides: \forall n,i,r.
 332 O < n \to
 333 p_ord n (nth_prime i) = pair nat nat O r
 334 \to Not (divides (nth_prime i) n).
 335 intros.
 336 lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
 337   [apply lt_SO_nth_prime_n
 338   |assumption
 339   |elim Hletin.
 340    simplify in H3.
 341    rewrite > H3.
 342    rewrite < plus_n_O.
 343    assumption
 344   ]
 345 qed.
 346
 347 theorem p_ord_to_not_eq_O : \forall n,p,q,r.
 348   (S O) < n \to
 349   p_ord n (nth_prime p) = pair nat nat q r \to
 350   Not (r=O).
 351 intros.
 352 unfold.intro.
 353 cut (O < n)
 354   [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
 355     [apply lt_SO_nth_prime_n.
 356     |assumption
 357     |elim Hletin.
 358      apply (lt_to_not_eq ? ? Hcut).
 359      rewrite > H4.
 360      rewrite > H2.
 361      apply times_n_O
 362     ]
 363   |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
 364   ]
 365 qed.
 366
 367 definition ord :nat \to nat \to nat \def
 368 \lambda n,p. fst ? ? (p_ord n p).
 369
 370 definition ord_rem :nat \to nat \to nat \def
 371 \lambda n,p. snd ? ? (p_ord n p).
 372
 373 theorem divides_to_ord: \forall p,n,m:nat.
 374 O < n \to O < m \to prime p
 375 \to divides n m
 376 \to divides (ord_rem n p) (ord_rem m p) \land (ord n p) \le (ord m p).
 377 intros.
 378 apply (divides_to_p_ord p ? ? ? ? n m H H1 H2 H3)
 379   [unfold ord.unfold ord_rem.apply eq_pair_fst_snd
 380   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
 381   ]
 382 qed.
 383
 384 theorem divides_to_divides_ord_rem: \forall p,n,m:nat.
 385 O < n \to O < m \to prime p \to divides n m \to
 386 divides (ord_rem n p) (ord_rem m p).
 387 intros.
 388 elim (divides_to_ord p n m H H1 H2 H3).assumption.
 389 qed.
 390
 391 theorem divides_to_le_ord: \forall p,n,m:nat.
 392 O < n \to O < m \to prime p \to divides n m \to
 393 (ord n p) \le (ord m p).
 394 intros.
 395 elim (divides_to_ord p n m H H1 H2 H3).assumption.
 396 qed.
 397
 398 theorem exp_ord: \forall p,n. (S O) \lt p
 399 \to O \lt n \to n = p \sup (ord n p) * (ord_rem n p).
 400 intros.
 401 elim (p_ord_to_exp1 p n (ord n p) (ord_rem n p))
 402   [assumption
 403   |assumption
 404   |assumption
 405   |unfold ord.unfold ord_rem.
 406    apply eq_pair_fst_snd
 407   ]
 408 qed.
 409
 410 theorem divides_ord_rem: \forall p,n. (S O) < p \to O < n
 411 \to divides (ord_rem n p) n.
 412 intros.
 413 apply (witness ? ? (p \sup (ord n p))).
 414 rewrite > sym_times.
 415 apply exp_ord[assumption|assumption]
 416 qed.
 417
 418 theorem lt_O_ord_rem: \forall p,n. (S O) < p \to O < n \to O < ord_rem n p.
 419 intros.
 420 elim (le_to_or_lt_eq O (ord_rem n p))
 421   [assumption
 422   |apply False_ind.
 423    apply (lt_to_not_eq ? ? H1).
 424    lapply (divides_ord_rem ? ? H H1).
 425    rewrite < H2 in Hletin.
 426    elim Hletin.
 427    rewrite > H3.
 428    reflexivity
 429   |apply le_O_n
 430   ]
 431 qed.
 432
 433 (* properties of ord e ord_rem *)
 434
 435 theorem ord_times: \forall p,m,n.O<m \to O<n \to prime p \to
 436 ord (m*n) p = ord m p+ord n p.
 437 intros.unfold ord.
 438 rewrite > (p_ord_times ? ? ? (ord m p) (ord_rem m p) (ord n p) (ord_rem n p))
 439   [reflexivity
 440   |assumption
 441   |assumption
 442   |assumption
 443   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
 444   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
 445   ]
 446 qed.
 447
 448 theorem ord_exp: \forall p,m.S O < p \to
 449 ord (exp p m) p = m.
 450 intros.
 451 unfold ord.
 452 rewrite > (p_ord_exp1 p (exp p m) m (S O))
 453   [reflexivity
 454   |apply lt_to_le.assumption
 455   |intro.apply (lt_to_not_le ? ? H).
 456    apply divides_to_le
 457     [apply lt_O_S
 458     |assumption
 459     ]
 460   |apply times_n_SO
 461   ]
 462 qed.
 463
 464 theorem not_divides_to_ord_O:
 465 \forall p,m. prime p \to \lnot (divides p m) \to
 466 ord m p = O.
 467 intros.unfold ord.
 468 rewrite > (p_ord_exp1 p m O m)
 469   [reflexivity
 470   |apply prime_to_lt_O.assumption
 471   |assumption
 472   |simplify.apply plus_n_O
 473   ]
 474 qed.
 475
 476 theorem ord_O_to_not_divides:
 477 \forall p,m. O < m \to prime p \to ord m p = O \to
 478 \lnot (divides p m).
 479 intros.
 480 lapply (p_ord_to_exp1 p m (ord m p) (ord_rem m p))
 481   [elim Hletin.
 482    rewrite > H4.
 483    rewrite > H2.
 484    rewrite > sym_times.
 485    rewrite < times_n_SO.
 486    assumption
 487   |apply prime_to_lt_SO.assumption
 488   |assumption
 489   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
 490   ]
 491 qed.
 492
 493 theorem divides_to_not_ord_O:
 494 \forall p,m. O < m \to prime p \to divides p m \to
 495 \lnot(ord m p = O).
 496 intros.intro.
 497 apply (ord_O_to_not_divides ? ? H H1 H3).
 498 assumption.
 499 qed.
 500
 501 theorem not_ord_O_to_divides:
 502 \forall p,m. O < m \to prime p \to \lnot (ord m p = O) \to
 503 divides p m.
 504 intros.
 505 rewrite > (exp_ord p) in ⊢ (? ? %)
 506   [apply (trans_divides ? (exp p (ord m p)))
 507     [generalize in match H2.
 508      cases (ord m p);intro
 509       [apply False_ind.apply H3.reflexivity
 510       |simplify.autobatch
 511       ]
 512     |autobatch
 513     ]
 514   |apply prime_to_lt_SO.
 515    assumption
 516   |assumption
 517   ]
 518 qed.
 519
 520 theorem not_divides_ord_rem: \forall m,p.O< m \to S O < p \to
 521 \lnot (divides p (ord_rem m p)).
 522 intros.
 523 elim (p_ord_to_exp1 p m (ord m p) (ord_rem m p))
 524   [assumption
 525   |assumption
 526   |assumption
 527   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
 528   ]
 529 qed.
 530
 531 theorem ord_ord_rem: \forall p,q,m. O < m \to
 532 prime p \to prime q \to
 533 q < p \to ord (ord_rem m p) q = ord m q.
 534 intros.
 535 rewrite > (exp_ord p) in ⊢ (? ? ? (? % ?))
 536   [rewrite > ord_times
 537     [rewrite > not_divides_to_ord_O in ⊢ (? ? ? (? % ?))
 538       [reflexivity
 539       |assumption
 540       |intro.
 541        apply (lt_to_not_eq ? ? H3).
 542        apply (divides_exp_to_eq ? ? ? H2 H1 H4)
 543       ]
 544     |apply lt_O_exp.
 545      apply (ltn_to_ltO ? ? H3)
 546     |apply lt_O_ord_rem
 547       [elim H1.assumption
 548       |assumption
 549
 550       ]
 551     |assumption
 552     ]
 553   |elim H1.assumption
 554   |assumption
 555   ]
 556 qed.
 557
 558 theorem lt_ord_rem: \forall n,m. prime n \to O < m \to
 559 divides n m \to ord_rem m n < m.
 560 intros.
 561 elim (le_to_or_lt_eq (ord_rem m n) m)
 562   [assumption
 563   |apply False_ind.
 564    apply (ord_O_to_not_divides ? ? H1 H ? H2).
 565    apply (inj_exp_r n)
 566     [apply prime_to_lt_SO.assumption
 567     |apply (inj_times_l1 m)
 568       [assumption
 569       |rewrite > sym_times in ⊢ (? ? ? %).
 570        rewrite < times_n_SO.
 571        rewrite < H3 in ⊢ (? ? (? ? %) ?).
 572        apply sym_eq.
 573        apply exp_ord
 574         [apply prime_to_lt_SO.assumption
 575         |assumption
 576         ]
 577       ]
 578     ]
 579   |apply divides_to_le
 580     [assumption
 581     |apply divides_ord_rem
 582       [apply prime_to_lt_SO.assumption
 583       |assumption
 584       ]
 585     ]
 586   ]
 587 qed.
 588
 589 (* p_ord_inv is used to encode the pair ord and rem into
 590    a single natural number. *)
 591
 592 definition p_ord_inv \def
 593 \lambda p,m,x.
 594   match p_ord x p with
 595   [pair q r \Rightarrow r*m+q].
 596
 597 theorem  eq_p_ord_inv: \forall p,m,x.
 598 p_ord_inv p m x = (ord_rem x p)*m+(ord x p).
 599 intros.unfold p_ord_inv. unfold ord_rem.
 600 unfold ord.
 601 elim (p_ord x p).
 602 reflexivity.
 603 qed.
 604
 605 theorem div_p_ord_inv:
 606 \forall p,m,x. ord x p < m \to p_ord_inv p m x / m = ord_rem x p.
 607 intros.rewrite > eq_p_ord_inv.
 608 apply div_plus_times.
 609 assumption.
 610 qed.
 611
 612 theorem mod_p_ord_inv:
 613 \forall p,m,x. ord x p < m \to p_ord_inv p m x \mod m = ord x p.
 614 intros.rewrite > eq_p_ord_inv.
 615 apply mod_plus_times.
 616 assumption.
 617 qed.