helm/software/matita/library/Q/ratio/rtimes.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 "Q/ratio/rinv.ma".
  16 include "Q/fraction/ftimes.ma".
  17
  18 definition rtimes : ratio → ratio → ratio ≝
  19 λr,s:ratio.
  20   match r with
  21   [one ⇒ s
  22   | (frac f) ⇒
  23       match s with
  24       [one ⇒ frac f
  25       | (frac g) ⇒ ftimes f g]].
  26
  27 theorem symmetric_rtimes : symmetric ratio rtimes.
  28 change with (∀r,s:ratio. rtimes r s = rtimes s r).
  29 intros.
  30 elim r. elim s.
  31 reflexivity.
  32 reflexivity.
  33 elim s.
  34 reflexivity.
  35 simplify.apply symmetric2_ftimes.
  36 qed.
  37
  38 variant sym_rtimes : ∀x,y:ratio. rtimes x y = rtimes y x ≝ symmetric_rtimes.
  39
  40 theorem rtimes_r_one: ∀r.rtimes r one = r.
  41  intro; cases r;reflexivity.
  42 qed.
  43
  44 theorem rtimes_one_r: ∀r.rtimes one r = r.
  45 intro; cases r;reflexivity.
  46 qed.
  47
  48 theorem rtimes_Zplus: \forall x,y.
  49 rtimes (nat_frac_item_to_ratio x) (nat_frac_item_to_ratio y) =
  50 nat_frac_item_to_ratio (x + y).
  51 intro.
  52 elim x
  53   [reflexivity
  54   |*:elim y;reflexivity
  55   ]
  56 qed.
  57
  58 theorem rtimes_Zplus1: \forall x,y,f.
  59 rtimes (nat_frac_item_to_ratio x) (frac (cons y f)) =
  60 frac (cons ((x + y)) f).
  61 intro.
  62 elim x
  63   [reflexivity
  64   |*:elim y;reflexivity
  65   ]
  66 qed.
  67
  68 theorem rtimes_Zplus2: \forall x,y,f.
  69 rtimes (frac (cons y f)) (nat_frac_item_to_ratio x) =
  70 frac (cons ((y + x)) f).
  71 intros.
  72 elim x
  73   [elim y;reflexivity
  74   |*:elim y;reflexivity
  75   ]
  76 qed.
  77
  78 theorem or_one_frac: \forall f,g.
  79 rtimes (frac f) (frac g) = one \lor
  80 \exists h.rtimes (frac f) (frac g) = frac h.
  81 intros.
  82 elim (rtimes (frac f) (frac g))
  83   [left.reflexivity
  84   |right.apply (ex_intro ? ? f1).reflexivity
  85   ]
  86 qed.
  87
  88 theorem one_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
  89 rtimes (frac f) (frac g) = one \to
  90 rtimes (frac (cons x f)) (frac (cons y g)) = nat_frac_item_to_ratio (x + y).
  91 intros.simplify.simplify in H.rewrite > H.simplify.
  92 reflexivity.
  93 qed.
  94
  95 theorem frac_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
  96 \forall h.rtimes (frac f) (frac g) = frac h \to
  97 rtimes (frac (cons x f)) (frac (cons y g)) = frac (cons (x + y) h).
  98 intros.simplify.simplify in H.rewrite > H.simplify.
  99 reflexivity.
 100 qed.
 101
 102
 103 theorem nat_frac_item_to_ratio_frac_frac: \forall z,f1,f2.
 104 rtimes (rtimes (nat_frac_item_to_ratio z) (frac f1)) (frac f2)
 105 =rtimes (nat_frac_item_to_ratio z) (rtimes (frac f1) (frac f2)).
 106 intros 2.elim f1
 107   [elim f2
 108     [change with
 109      (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (pos n1))
 110       =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_to_ratio (pos n1)))).
 111      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 112      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 113      rewrite > assoc_Zplus.reflexivity
 114     |change with
 115      (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (neg n1))
 116       =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_to_ratio (neg n1)))).
 117      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 118      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 119      rewrite > assoc_Zplus.reflexivity
 120     |change with
 121       (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (pos n))) (frac (cons z1 f))
 122        = rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (pos n)) (frac (cons z1 f)))).
 123      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
 124      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
 125      rewrite > assoc_Zplus.reflexivity
 126     ]
 127   |elim f2
 128     [change with
 129      (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (pos n1))
 130       =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_to_ratio (pos n1)))).
 131      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 132      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 133      rewrite > assoc_Zplus.reflexivity
 134     |change with
 135      (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (neg n1))
 136       =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_to_ratio (neg n1)))).
 137      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 138      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 139      rewrite > assoc_Zplus.reflexivity
 140     |change with
 141       (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (neg n))) (frac (cons z1 f))
 142        = rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (neg n)) (frac (cons z1 f)))).
 143      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
 144      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
 145      rewrite > assoc_Zplus.reflexivity
 146     ]
 147   |elim f2
 148     [change with
 149      (rtimes (rtimes (nat_frac_item_to_ratio z) (frac (cons z1 f))) (nat_frac_item_to_ratio (pos n))
 150       =rtimes (nat_frac_item_to_ratio z) (rtimes (frac (cons z1 f)) (nat_frac_item_to_ratio (pos n)))).
 151      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
 152      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
 153      rewrite > assoc_Zplus.reflexivity
 154     |change with
 155      (rtimes (rtimes (nat_frac_item_to_ratio z) (frac (cons z1 f))) (nat_frac_item_to_ratio (neg n))
 156       =rtimes (nat_frac_item_to_ratio z) (rtimes (frac (cons z1 f)) (nat_frac_item_to_ratio (neg n)))).
 157      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
 158      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
 159      rewrite > assoc_Zplus.reflexivity
 160     |elim (or_one_frac f f3)
 161       [rewrite > rtimes_Zplus1.
 162        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 163        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 164        rewrite > rtimes_Zplus.
 165        rewrite > assoc_Zplus.reflexivity
 166       |elim H2.clear H2.
 167        rewrite > rtimes_Zplus1.
 168        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
 169        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
 170        rewrite > rtimes_Zplus1.
 171        rewrite > assoc_Zplus.reflexivity
 172       ]
 173     ]
 174   ]
 175 qed.
 176
 177 theorem cons_frac_frac: \forall f1,z,f,f2.
 178 rtimes (rtimes (frac (cons z f)) (frac f1)) (frac f2)
 179 =rtimes (frac (cons z f)) (rtimes (frac f1) (frac f2)).
 180 intro.elim f1
 181   [elim f2
 182     [change with
 183      (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (pos n1))
 184       =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_to_ratio (pos n1)))).
 185      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
 186      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
 187      rewrite > assoc_Zplus.reflexivity
 188     |change with
 189      (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (neg n1))
 190       =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_to_ratio (neg n1)))).
 191      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
 192      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
 193      rewrite > assoc_Zplus.reflexivity
 194     |change with
 195       (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (pos n))) (frac (cons z1 f3))
 196        = rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (pos n)) (frac (cons z1 f3)))).
 197      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
 198      elim (or_one_frac f f3)
 199       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 200        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 201        rewrite > assoc_Zplus.reflexivity
 202       |elim H1.clear H1.
 203        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 204        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 205        rewrite > assoc_Zplus.reflexivity
 206       ]
 207     ]
 208   |elim f2
 209     [change with
 210      (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (pos n1))
 211       =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_to_ratio (pos n1)))).
 212      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
 213      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
 214      rewrite > assoc_Zplus.reflexivity
 215     |change with
 216      (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (neg n1))
 217       =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_to_ratio (neg n1)))).
 218      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
 219      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
 220      rewrite > assoc_Zplus.reflexivity
 221     |change with
 222       (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (neg n))) (frac (cons z1 f3))
 223        = rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (neg n)) (frac (cons z1 f3)))).
 224      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
 225      elim (or_one_frac f f3)
 226       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 227        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 228        rewrite > assoc_Zplus.reflexivity
 229       |elim H1.clear H1.
 230        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 231        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 232        rewrite > assoc_Zplus.reflexivity
 233       ]
 234     ]
 235   |elim f3
 236     [change with
 237      (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (nat_frac_item_to_ratio (pos n))
 238       =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (pos n)))).
 239      rewrite > rtimes_Zplus2.
 240      elim (or_one_frac f2 f)
 241       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 242        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 243        rewrite > rtimes_Zplus.
 244        rewrite > assoc_Zplus.reflexivity
 245       |elim H1.clear H1.
 246        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 247        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 248        rewrite > rtimes_Zplus2.
 249        rewrite > assoc_Zplus.reflexivity
 250       ]
 251     |change with
 252      (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (nat_frac_item_to_ratio (neg n))
 253       =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (neg n)))).
 254      rewrite > rtimes_Zplus2.
 255      elim (or_one_frac f2 f)
 256       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 257        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 258        rewrite > rtimes_Zplus.
 259        rewrite > assoc_Zplus.reflexivity
 260       |elim H1.clear H1.
 261        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 262        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 263        rewrite > rtimes_Zplus2.
 264        rewrite > assoc_Zplus.reflexivity
 265       ]
 266     |elim (or_one_frac f2 f)
 267       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 268        rewrite > rtimes_Zplus1.
 269        elim (or_one_frac f f4)
 270         [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H3).
 271          rewrite > rtimes_Zplus2.
 272          cut (f4 = f2)
 273           [rewrite > Hcut.
 274            rewrite > assoc_Zplus.reflexivity
 275           |apply injective_frac.
 276            rewrite < rtimes_one_r.
 277            rewrite < H2.
 278            (* problema inaspettato: mi serve l'unicita' dell'inversa,
 279               che richiede (?) l'associativita. Per fortuna basta
 280               l'ipotesi induttiva. *)
 281            cases f2
 282             [change with
 283              (rtimes (rtimes (nat_frac_item_to_ratio (pos n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (pos n)).
 284              rewrite > nat_frac_item_to_ratio_frac_frac.
 285              rewrite > H3.
 286              rewrite > rtimes_r_one.
 287              reflexivity
 288             |change with
 289              (rtimes (rtimes (nat_frac_item_to_ratio (neg n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (neg n)).
 290              rewrite > nat_frac_item_to_ratio_frac_frac.
 291              rewrite > H3.
 292              rewrite > rtimes_r_one.
 293              reflexivity
 294             |rewrite > H.
 295              rewrite > H3.
 296              rewrite > rtimes_r_one.
 297              reflexivity
 298             ]
 299           ]
 300         |elim H3.clear H3.
 301          rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H4).
 302          cut (rtimes (frac f2) (frac a) = frac f4)
 303           [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f4 Hcut).
 304            rewrite > assoc_Zplus.reflexivity
 305           |rewrite < H4.
 306            generalize in match H2.
 307            cases f2;intro
 308             [change with
 309              (rtimes (nat_frac_item_to_ratio (pos n)) (rtimes (frac f)(frac f4)) =frac f4).
 310              rewrite < nat_frac_item_to_ratio_frac_frac.
 311              rewrite > H3.
 312              rewrite > rtimes_one_r.
 313              reflexivity
 314             |change with
 315              (rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f)(frac f4)) =frac f4).
 316              rewrite < nat_frac_item_to_ratio_frac_frac.
 317              rewrite > H3.
 318              rewrite > rtimes_one_r.
 319              reflexivity
 320             |rewrite < H.
 321              rewrite > H3.
 322              rewrite > rtimes_one_r.
 323              reflexivity
 324             ]
 325           ]
 326         ]
 327       |elim H2.clear H2.
 328        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
 329        elim (or_one_frac f f4)
 330         [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 331          rewrite > rtimes_Zplus2.
 332          cut (rtimes (frac a) (frac f4) = frac f2)
 333           [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f2 Hcut).
 334            rewrite > assoc_Zplus.reflexivity
 335           |rewrite < H3.
 336            generalize in match H2.
 337            cases f2;intro
 338             [change with
 339              (rtimes (rtimes (nat_frac_item_to_ratio (pos n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (pos n)).
 340              rewrite > nat_frac_item_to_ratio_frac_frac.
 341              rewrite > H4.
 342              rewrite > rtimes_r_one.
 343              reflexivity
 344             |change with
 345              (rtimes (rtimes (nat_frac_item_to_ratio (neg n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (neg n)).
 346              rewrite > nat_frac_item_to_ratio_frac_frac.
 347              rewrite > H4.
 348              rewrite > rtimes_r_one.
 349              reflexivity
 350             |rewrite > H.
 351              rewrite > H4.
 352              rewrite > rtimes_r_one.
 353              reflexivity
 354             ]
 355           ]
 356         |elim H2.clear H2.
 357          rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a1 H4).
 358          elim (or_one_frac a f4)
 359           [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 360            cut (rtimes (frac f2) (frac a1) = one)
 361             [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? Hcut).
 362              rewrite > assoc_Zplus.reflexivity
 363             |rewrite < H4.
 364              generalize in match H3.
 365              cases f2;intro
 366               [change with
 367                (rtimes (nat_frac_item_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = one).
 368                rewrite < nat_frac_item_to_ratio_frac_frac.
 369                rewrite > H5.
 370                assumption
 371               |change with
 372                (rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = one).
 373                rewrite < nat_frac_item_to_ratio_frac_frac.
 374                rewrite > H5.
 375                assumption
 376               |rewrite < H.
 377                rewrite > H5.
 378                assumption
 379               ]
 380             ]
 381           |elim H2.clear H2.
 382            rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 H5).
 383            cut (rtimes (frac f2) (frac a1) = frac a2)
 384             [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 Hcut).
 385              rewrite > assoc_Zplus.reflexivity
 386             |rewrite < H4.
 387              generalize in match H3.
 388              cases f2;intro
 389               [change with
 390                (rtimes (nat_frac_item_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = frac a2).
 391                rewrite < nat_frac_item_to_ratio_frac_frac.
 392                rewrite > H2.
 393                assumption
 394               |change with
 395                (rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = frac a2).
 396                rewrite < nat_frac_item_to_ratio_frac_frac.
 397                rewrite > H2.
 398                assumption
 399               |rewrite < H.
 400                rewrite > H2.
 401                assumption
 402               ]
 403             ]
 404           ]
 405         ]
 406       ]
 407     ]
 408   ]
 409 qed.
 410
 411 theorem frac_frac_fracaux: ∀f,f1,f2.
 412 rtimes (rtimes (frac f) (frac f1)) (frac f2)
 413 =rtimes (frac f) (rtimes (frac f1) (frac f2)).
 414 intros.
 415 cases f
 416   [change with
 417    (rtimes (rtimes (nat_frac_item_to_ratio (pos n)) (frac f1)) (frac f2)
 418     =rtimes (nat_frac_item_to_ratio (pos n)) (rtimes (frac f1) (frac f2))).
 419    apply nat_frac_item_to_ratio_frac_frac
 420   |change with
 421    (rtimes (rtimes (nat_frac_item_to_ratio (neg n)) (frac f1)) (frac f2)
 422     =rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f1) (frac f2))).
 423    apply nat_frac_item_to_ratio_frac_frac
 424   |apply cons_frac_frac]
 425 qed.
 426
 427
 428 theorem associative_rtimes:associative ? rtimes.
 429 unfold.intros.
 430 cases x
 431   [reflexivity
 432   |cases y
 433     [reflexivity.
 434     |cases z
 435       [rewrite > rtimes_r_one.rewrite > rtimes_r_one.reflexivity
 436       |apply frac_frac_fracaux
 437       ]]]
 438 qed.
 439
 440
 441 theorem rtimes_rinv: ∀r:ratio. rtimes r (rinv r) = one.
 442 intro.elim r.
 443 reflexivity.
 444 simplify.apply ftimes_finv.
 445 qed.
 446
 447 theorem rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
 448 (rtimes (frac f) (frac g) = one \land
 449  rtimes (frac (cons x f)) (frac (cons y g)) = nat_frac_item_to_ratio (x + y))
 450 \lor (\exists h.rtimes (frac f) (frac g) = frac h \land
 451 rtimes (frac (cons x f)) (frac (cons y g)) =
 452 frac (cons (x + y) h)).
 453 intros.
 454 simplify.
 455 elim (rtimes (frac f) (frac g));simplify
 456   [left.split;reflexivity
 457   |right.
 458    apply (ex_intro ? ? f1).
 459    split;reflexivity]
 460 qed.