helm/software/matita/library/Q/frac.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/Q/frac".
  16
  17 include "nat/factorization.ma".
  18 include "Q/q.ma".
  19
  20 (* transformation from nat_fact to fracion *)
  21 let rec nat_fact_to_fraction l \def
  22   match l with
  23   [nf_last a \Rightarrow pp a
  24   |nf_cons a p \Rightarrow
  25     cons (Z_of_nat a) (nat_fact_to_fraction p)
  26   ]
  27 .
  28
  29 (* returns the numerator of a fraction in the form of a nat_fact_all *)
  30 let rec numerator f \def
  31   match f with
  32   [pp a \Rightarrow nfa_proper (nf_last a)
  33   |nn a \Rightarrow nfa_one
  34   |cons a l \Rightarrow
  35     let n \def numerator l in
  36     match n with
  37     [nfa_zero \Rightarrow (* this case is vacuous *) nfa_zero
  38     |nfa_one  \Rightarrow
  39       match a with
  40       [OZ \Rightarrow nfa_one
  41       |pos x \Rightarrow nfa_proper (nf_last x)
  42       |neg x \Rightarrow nfa_one
  43       ]
  44     |nfa_proper g \Rightarrow
  45       match a with
  46       [OZ \Rightarrow nfa_proper (nf_cons O g)
  47       |pos x \Rightarrow nfa_proper (nf_cons (S x) g)
  48       |neg x \Rightarrow nfa_proper (nf_cons O g)
  49       ]
  50     ]
  51   ]
  52 .
  53
  54 theorem not_eq_numerator_nfa_zero:
  55 \forall f.numerator f \neq nfa_zero.
  56 intro.elim f
  57   [simplify.intro.destruct H
  58   |simplify.intro.destruct H
  59   |simplify.generalize in match H.
  60    cases (numerator f1)
  61     [intro.elim H1.reflexivity
  62     |simplify.intro.
  63      cases z;simplify;intro;destruct H2
  64     |simplify.intro.
  65      cases z;simplify;intro;destruct H2
  66     ]
  67   ]
  68 qed.
  69
  70 theorem or_numerator_nfa_one_nfa_proper:
  71 \forall f.(numerator f = nfa_one \land \exists g.numerator (finv f) =
  72 nfa_proper g) \lor \exists g.numerator f = nfa_proper g.
  73 intro.elim f
  74   [simplify.right.
  75    apply (ex_intro ? ? (nf_last n)).reflexivity
  76   |simplify.left.split
  77     [reflexivity
  78     |apply (ex_intro ? ? (nf_last n)).reflexivity
  79     ]
  80   |elim H;clear H
  81     [elim H1.clear H1.
  82      elim H2.clear H2.
  83      elim z
  84       [simplify.
  85        rewrite > H.rewrite > H1.simplify.
  86        left.split
  87         [reflexivity
  88         |apply (ex_intro ? ? (nf_cons O a)).reflexivity
  89         ]
  90       |simplify.
  91        rewrite > H.rewrite > H1.simplify.
  92        right.apply (ex_intro ? ? (nf_last n)).reflexivity
  93       |simplify.
  94        rewrite > H.rewrite > H1.simplify.
  95        left.split
  96         [reflexivity
  97         |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
  98         ]
  99       ]
 100     |elim H1.clear H1.
 101       elim z
 102       [simplify.
 103        rewrite > H.simplify.
 104        right.
 105        apply (ex_intro ? ? (nf_cons O a)).reflexivity
 106       |simplify.
 107        rewrite > H.simplify.
 108        right.apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
 109       |simplify.
 110        rewrite > H.simplify.
 111        right.
 112        apply (ex_intro ? ? (nf_cons O a)).reflexivity
 113       ]
 114     ]
 115   ]
 116 qed.
 117
 118 theorem eq_nfa_one_to_eq_finv_nfa_proper:
 119 \forall f.numerator f = nfa_one \to
 120 \exist h.numerator (finv f) = nfa_proper h.
 121 intro.elim f
 122   [simplify in H.destruct H
 123   |simplify.apply (ex_intro ? ? (nf_last n)).reflexivity
 124   |generalize in match H1.clear H1.
 125    generalize in match H.clear H.
 126    simplify.
 127    cases (numerator f1);simplify
 128     [intros;destruct H1
 129     |intros;elim (H (refl_eq ? ?)).
 130      rewrite > H2.simplify.
 131      elim z;simplify
 132       [apply (ex_intro ? ? (nf_cons O a)).reflexivity
 133       |apply (ex_intro ? ? (nf_cons O a)).reflexivity
 134       |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
 135       ]
 136     |elim z;destruct H1
 137     ]
 138   ]
 139 qed.
 140
 141 theorem numerator_nat_fact_to_fraction: \forall g:nat_fact.
 142 numerator (nat_fact_to_fraction g) = nfa_proper g.
 143 intro.
 144 elim g
 145   [simplify.reflexivity.
 146   |simplify.rewrite > H.simplify.
 147    cases n;reflexivity
 148   ]
 149 qed.
 150
 151 definition numeratorQ \def
 152 \lambda q.match q with
 153   [OQ \Rightarrow nfa_zero
 154   |pos r \Rightarrow
 155     match r with
 156     [one \Rightarrow nfa_one
 157     |frac x \Rightarrow numerator x
 158     ]
 159   |neg r \Rightarrow
 160     match r with
 161     [one \Rightarrow nfa_one
 162     |frac x \Rightarrow numerator x
 163     ]
 164   ]
 165 .
 166
 167 definition nat_fact_all_to_Q \def
 168 \lambda n.
 169   match n with
 170   [nfa_zero \Rightarrow OQ
 171   |nfa_one \Rightarrow Qpos one
 172   |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction l))
 173   ]
 174 .
 175
 176 theorem numeratorQ_nat_fact_all_to_Q: \forall g.
 177 numeratorQ (nat_fact_all_to_Q g) = g.
 178 intro.cases g
 179   [reflexivity
 180   |reflexivity
 181   |apply numerator_nat_fact_to_fraction
 182   ]
 183 qed.
 184
 185 definition nat_to_Q \def
 186 \lambda n. nat_fact_all_to_Q (factorize n).
 187
 188 let rec nat_fact_to_fraction_inv l \def
 189   match l with
 190   [nf_last a \Rightarrow nn a
 191   |nf_cons a p \Rightarrow
 192     cons (neg_Z_of_nat a) (nat_fact_to_fraction_inv p)
 193   ]
 194 .
 195
 196 (*
 197 definition nat_fact_all_to_Q_inv \def
 198 \lambda n.
 199   match n with
 200   [nfa_zero \Rightarrow OQ
 201   |nfa_one \Rightarrow Qpos one
 202   |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction_inv l))
 203   ]
 204 .
 205
 206 definition nat_to_Q_inv \def
 207 \lambda n. nat_fact_all_to_Q_inv (factorize n).
 208 *)
 209
 210 definition Qinv \def
 211 \lambda q.match q with
 212 [OQ \Rightarrow OQ
 213 |Qpos r \Rightarrow Qpos (rinv r)
 214 |Qneg r \Rightarrow Qneg (rinv r)
 215 ].
 216
 217 definition frac:nat \to nat \to Q \def
 218 \lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
 219
 220 theorem rtimes_oner: \forall r.rtimes r one = r.
 221 intro.cases r;reflexivity.
 222 qed.
 223
 224 theorem rtimes_onel: \forall r.rtimes one r = r.
 225 intro.cases r;reflexivity.
 226 qed.
 227
 228 definition Qone \def Qpos one.
 229
 230 theorem Qtimes_Qoner: \forall q.Qtimes q Qone = q.
 231 intro.cases q
 232   [reflexivity
 233   |cases r
 234     [reflexivity
 235     |reflexivity
 236     ]
 237   |cases r
 238     [reflexivity
 239     |reflexivity
 240     ]
 241   ]
 242 qed.
 243
 244 theorem Qtimes_Qonel: \forall q.Qtimes Qone q = q.
 245 intros.cases q
 246   [reflexivity
 247   |cases r
 248     [reflexivity
 249     |reflexivity
 250     ]
 251   |cases r
 252     [reflexivity
 253     |reflexivity
 254     ]
 255   ]
 256 qed.
 257
 258 let rec times_f h g \def
 259   match h with
 260   [nf_last a \Rightarrow
 261     match g with
 262     [nf_last b \Rightarrow nf_last (S (a+b))
 263     |nf_cons b g1 \Rightarrow nf_cons (S (a+b)) g1
 264     ]
 265   |nf_cons a h1 \Rightarrow
 266     match g with
 267     [nf_last b \Rightarrow nf_cons (S (a+b)) h1
 268     |nf_cons b g1 \Rightarrow nf_cons (a+b) (times_f h1 g1)
 269     ]
 270   ]
 271 .
 272
 273 definition times_fa \def
 274 \lambda f,g.
 275 match f with
 276 [nfa_zero \Rightarrow nfa_zero
 277 |nfa_one \Rightarrow g
 278 |nfa_proper f1 \Rightarrow match g with
 279   [nfa_zero \Rightarrow nfa_zero
 280   |nfa_one \Rightarrow nfa_proper f1
 281   |nfa_proper g1 \Rightarrow nfa_proper (times_f f1 g1)
 282   ]
 283 ]
 284 .
 285
 286 theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
 287 =defactorize_aux g m*defactorize_aux h m.
 288 intro.elim g
 289   [elim h;simplify;autobatch
 290   |elim h
 291     [simplify;autobatch
 292     |simplify.rewrite > (H n3 (S m)).autobatch
 293     ]
 294   ]
 295 qed.
 296
 297 theorem eq_times_fa_times: \forall f,g.
 298 defactorize (times_fa f g) = defactorize f*defactorize g.
 299 intros.
 300 elim f
 301   [reflexivity
 302   |simplify.apply plus_n_O
 303   |elim g;simplify
 304     [apply times_n_O
 305     |apply times_n_SO
 306     |apply eq_times_f_times1
 307     ]
 308   ]
 309 qed.
 310
 311 theorem eq_times_times_fa: \forall n,m.
 312 factorize (n*m) = times_fa (factorize n) (factorize m).
 313 intros.
 314 rewrite <(factorize_defactorize (times_fa (factorize n) (factorize m))).
 315 rewrite > eq_times_fa_times.
 316 rewrite > defactorize_factorize.
 317 rewrite > defactorize_factorize.
 318 reflexivity.
 319 qed.
 320
 321
 322 theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) =
 323 Z_of_nat n + Z_of_nat m.
 324 intro.cases n;intro
 325   [reflexivity
 326   |cases m
 327     [simplify.rewrite < plus_n_O.reflexivity
 328     |simplify.reflexivity.
 329     ]
 330   ]
 331 qed.
 332
 333 definition unfrac \def \lambda f.
 334 match f with
 335   [one \Rightarrow pp O
 336   |frac f \Rightarrow f
 337   ]
 338 .
 339
 340 lemma injective_frac: injective fraction ratio frac.
 341 unfold.intros.
 342 change with ((unfrac (frac x)) = (unfrac (frac y))).
 343 rewrite < H.reflexivity.
 344 qed.
 345
 346 theorem times_f_ftimes: \forall n,m.
 347 frac (nat_fact_to_fraction (times_f n m))
 348 = ftimes (nat_fact_to_fraction n) (nat_fact_to_fraction m).
 349 intro.
 350 elim n
 351   [elim m
 352     [simplify.
 353      rewrite < plus_n_Sm.reflexivity
 354     |elim n2
 355       [simplify.rewrite < plus_n_O.reflexivity
 356       |simplify.reflexivity.
 357       ]
 358     ]
 359   |elim m
 360     [elim n1
 361       [simplify.reflexivity
 362       |simplify.rewrite < plus_n_Sm.reflexivity
 363       ]
 364     |simplify.
 365      cut (\exist h.ftimes (nat_fact_to_fraction n2) (nat_fact_to_fraction n4) = frac h)
 366       [elim Hcut.
 367        rewrite > H2.
 368        simplify.apply eq_f.
 369        apply eq_f2
 370         [apply eq_plus_Zplus
 371         |apply injective_frac.
 372          rewrite < H2.
 373          apply H
 374         ]
 375       |generalize in match n4.
 376        elim n2
 377         [cases n6;simplify;autobatch
 378         |cases n7;simplify
 379           [autobatch
 380           |elim (H2 n9).
 381            rewrite > H3.
 382            simplify.
 383            autobatch
 384           ]
 385         ]
 386       ]
 387     ]
 388   ]
 389 qed.
 390
 391 theorem times_fa_Qtimes: \forall f,g. nat_fact_all_to_Q (times_fa f g) =
 392 Qtimes (nat_fact_all_to_Q f) (nat_fact_all_to_Q g).
 393 intros.
 394 cases f;simplify
 395   [reflexivity
 396   |cases g;reflexivity
 397   |cases g;simplify
 398     [reflexivity
 399     |reflexivity
 400     |rewrite > times_f_ftimes.reflexivity
 401     ]
 402   ]
 403 qed.
 404
 405 theorem times_Qtimes: \forall p,q.
 406 (nat_to_Q (p*q)) = Qtimes (nat_to_Q p) (nat_to_Q q).
 407 intros.unfold nat_to_Q.
 408 rewrite < times_fa_Qtimes.
 409 rewrite < eq_times_times_fa.
 410 reflexivity.
 411 qed.
 412
 413 theorem rtimes_Zplus: \forall x,y.
 414 rtimes (Z_to_ratio x) (Z_to_ratio y) =
 415 Z_to_ratio (x + y).
 416 intro.
 417 elim x
 418   [reflexivity
 419   |elim y;reflexivity
 420   |elim y;reflexivity
 421   ]
 422 qed.
 423
 424 theorem rtimes_Zplus1: \forall x,y,f.
 425 rtimes (Z_to_ratio x) (frac (cons y f)) =
 426 frac (cons ((x + y)) f).
 427 intro.
 428 elim x
 429   [reflexivity
 430   |elim y;reflexivity
 431   |elim y;reflexivity
 432   ]
 433 qed.
 434
 435 theorem rtimes_Zplus2: \forall x,y,f.
 436 rtimes (frac (cons y f)) (Z_to_ratio x) =
 437 frac (cons ((y + x)) f).
 438 intros.
 439 elim x
 440   [elim y;reflexivity
 441   |elim y;reflexivity
 442   |elim y;reflexivity
 443   ]
 444 qed.
 445
 446 theorem or_one_frac: \forall f,g.
 447 rtimes (frac f) (frac g) = one \lor
 448 \exists h.rtimes (frac f) (frac g) = frac h.
 449 intros.
 450 elim (rtimes (frac f) (frac g))
 451   [left.reflexivity
 452   |right.apply (ex_intro ? ? f1).reflexivity
 453   ]
 454 qed.
 455
 456 theorem one_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
 457 rtimes (frac f) (frac g) = one \to
 458 rtimes (frac (cons x f)) (frac (cons y g)) = Z_to_ratio (x + y).
 459 intros.simplify.simplify in H.rewrite > H.simplify.
 460 reflexivity.
 461 qed.
 462
 463 theorem frac_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
 464 \forall h.rtimes (frac f) (frac g) = frac h \to
 465 rtimes (frac (cons x f)) (frac (cons y g)) = frac (cons (x + y) h).
 466 intros.simplify.simplify in H.rewrite > H.simplify.
 467 reflexivity.
 468 qed.
 469
 470 theorem rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
 471 (rtimes (frac f) (frac g) = one \land
 472  rtimes (frac (cons x f)) (frac (cons y g)) = Z_to_ratio (x + y))
 473 \lor (\exists h.rtimes (frac f) (frac g) = frac h \land
 474 rtimes (frac (cons x f)) (frac (cons y g)) =
 475 frac (cons (x + y) h)).
 476 intros.
 477 simplify.
 478 elim (rtimes (frac f) (frac g));simplify
 479   [left.split;reflexivity
 480   |right.
 481    apply (ex_intro ? ? f1).
 482    split;reflexivity
 483   ]
 484 qed.
 485
 486 theorem Z_to_ratio_frac_frac: \forall z,f1,f2.
 487 rtimes (rtimes (Z_to_ratio z) (frac f1)) (frac f2)
 488 =rtimes (Z_to_ratio z) (rtimes (frac f1) (frac f2)).
 489 intros 2.elim f1
 490   [elim f2
 491     [change with
 492      (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (Z_to_ratio (pos n1))
 493       =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (pos n1)))).
 494      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 495      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 496      rewrite > assoc_Zplus.reflexivity
 497     |change with
 498      (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (Z_to_ratio (neg n1))
 499       =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (neg n1)))).
 500      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 501      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 502      rewrite > assoc_Zplus.reflexivity
 503     |change with
 504       (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (frac (cons z1 f))
 505        = rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (frac (cons z1 f)))).
 506      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
 507      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
 508      rewrite > assoc_Zplus.reflexivity
 509     ]
 510   |elim f2
 511     [change with
 512      (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (Z_to_ratio (pos n1))
 513       =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (pos n1)))).
 514      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 515      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 516      rewrite > assoc_Zplus.reflexivity
 517     |change with
 518      (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (Z_to_ratio (neg n1))
 519       =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (neg n1)))).
 520      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 521      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 522      rewrite > assoc_Zplus.reflexivity
 523     |change with
 524       (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (frac (cons z1 f))
 525        = rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (frac (cons z1 f)))).
 526      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
 527      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
 528      rewrite > assoc_Zplus.reflexivity
 529     ]
 530   |elim f2
 531     [change with
 532      (rtimes (rtimes (Z_to_ratio z) (frac (cons z1 f))) (Z_to_ratio (pos n))
 533       =rtimes (Z_to_ratio z) (rtimes (frac (cons z1 f)) (Z_to_ratio (pos n)))).
 534      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
 535      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
 536      rewrite > assoc_Zplus.reflexivity
 537     |change with
 538      (rtimes (rtimes (Z_to_ratio z) (frac (cons z1 f))) (Z_to_ratio (neg n))
 539       =rtimes (Z_to_ratio z) (rtimes (frac (cons z1 f)) (Z_to_ratio (neg n)))).
 540      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
 541      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
 542      rewrite > assoc_Zplus.reflexivity
 543     |elim (or_one_frac f f3)
 544       [rewrite > rtimes_Zplus1.
 545        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 546        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 547        rewrite > rtimes_Zplus.
 548        rewrite > assoc_Zplus.reflexivity
 549       |elim H2.clear H2.
 550        rewrite > rtimes_Zplus1.
 551        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
 552        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
 553        rewrite > rtimes_Zplus1.
 554        rewrite > assoc_Zplus.reflexivity
 555       ]
 556     ]
 557   ]
 558 qed.
 559
 560 theorem cons_frac_frac: \forall f1,z,f,f2.
 561 rtimes (rtimes (frac (cons z f)) (frac f1)) (frac f2)
 562 =rtimes (frac (cons z f)) (rtimes (frac f1) (frac f2)).
 563 intro.elim f1
 564   [elim f2
 565     [change with
 566      (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (Z_to_ratio (pos n1))
 567       =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (pos n1)))).
 568      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
 569      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
 570      rewrite > assoc_Zplus.reflexivity
 571     |change with
 572      (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (Z_to_ratio (neg n1))
 573       =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (neg n1)))).
 574      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
 575      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
 576      rewrite > assoc_Zplus.reflexivity
 577     |change with
 578       (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (frac (cons z1 f3))
 579        = rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (frac (cons z1 f3)))).
 580      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
 581      elim (or_one_frac f f3)
 582       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 583        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 584        rewrite > assoc_Zplus.reflexivity
 585       |elim H1.clear H1.
 586        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 587        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 588        rewrite > assoc_Zplus.reflexivity
 589       ]
 590     ]
 591   |elim f2
 592     [change with
 593      (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (Z_to_ratio (pos n1))
 594       =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (pos n1)))).
 595      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
 596      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
 597      rewrite > assoc_Zplus.reflexivity
 598     |change with
 599      (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (Z_to_ratio (neg n1))
 600       =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (neg n1)))).
 601      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
 602      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
 603      rewrite > assoc_Zplus.reflexivity
 604     |change with
 605       (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (frac (cons z1 f3))
 606        = rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (frac (cons z1 f3)))).
 607      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
 608      elim (or_one_frac f f3)
 609       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 610        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 611        rewrite > assoc_Zplus.reflexivity
 612       |elim H1.clear H1.
 613        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 614        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 615        rewrite > assoc_Zplus.reflexivity
 616       ]
 617     ]
 618   |elim f3
 619     [change with
 620      (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (Z_to_ratio (pos n))
 621       =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (Z_to_ratio (pos n)))).
 622      rewrite > rtimes_Zplus2.
 623      elim (or_one_frac f2 f)
 624       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 625        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 626        rewrite > rtimes_Zplus.
 627        rewrite > assoc_Zplus.reflexivity
 628       |elim H1.clear H1.
 629        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 630        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 631        rewrite > rtimes_Zplus2.
 632        rewrite > assoc_Zplus.reflexivity
 633       ]
 634     |change with
 635      (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (Z_to_ratio (neg n))
 636       =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (Z_to_ratio (neg n)))).
 637      rewrite > rtimes_Zplus2.
 638      elim (or_one_frac f2 f)
 639       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 640        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 641        rewrite > rtimes_Zplus.
 642        rewrite > assoc_Zplus.reflexivity
 643       |elim H1.clear H1.
 644        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 645        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 646        rewrite > rtimes_Zplus2.
 647        rewrite > assoc_Zplus.reflexivity
 648       ]
 649     |elim (or_one_frac f2 f)
 650       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 651        rewrite > rtimes_Zplus1.
 652        elim (or_one_frac f f4)
 653         [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H3).
 654          rewrite > rtimes_Zplus2.
 655          cut (f4 = f2)
 656           [rewrite > Hcut.
 657            rewrite > assoc_Zplus.reflexivity
 658           |apply injective_frac.
 659            rewrite < rtimes_onel.
 660            rewrite < H2.
 661            (* problema inaspettato: mi serve l'unicita' dell'inversa,
 662               che richiede (?) l'associativita. Per fortuna basta
 663               l'ipotesi induttiva. *)
 664            cases f2
 665             [change with
 666              (rtimes (rtimes (Z_to_ratio (pos n)) (frac f)) (frac f4)=Z_to_ratio (pos n)).
 667              rewrite > Z_to_ratio_frac_frac.
 668              rewrite > H3.
 669              rewrite > rtimes_oner.
 670              reflexivity
 671             |change with
 672              (rtimes (rtimes (Z_to_ratio (neg n)) (frac f)) (frac f4)=Z_to_ratio (neg n)).
 673              rewrite > Z_to_ratio_frac_frac.
 674              rewrite > H3.
 675              rewrite > rtimes_oner.
 676              reflexivity
 677             |rewrite > H.
 678              rewrite > H3.
 679              rewrite > rtimes_oner.
 680              reflexivity
 681             ]
 682           ]
 683         |elim H3.clear H3.
 684          rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H4).
 685          cut (rtimes (frac f2) (frac a) = frac f4)
 686           [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f4 Hcut).
 687            rewrite > assoc_Zplus.reflexivity
 688           |rewrite < H4.
 689            generalize in match H2.
 690            cases f2;intro
 691             [change with
 692              (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) =frac f4).
 693              rewrite < Z_to_ratio_frac_frac.
 694              rewrite > H3.
 695              rewrite > rtimes_onel.
 696              reflexivity
 697             |change with
 698              (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) =frac f4).
 699              rewrite < Z_to_ratio_frac_frac.
 700              rewrite > H3.
 701              rewrite > rtimes_onel.
 702              reflexivity
 703             |rewrite < H.
 704              rewrite > H3.
 705              rewrite > rtimes_onel.
 706              reflexivity
 707             ]
 708           ]
 709         ]
 710       |elim H2.clear H2.
 711        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
 712        elim (or_one_frac f f4)
 713         [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 714          rewrite > rtimes_Zplus2.
 715          cut (rtimes (frac a) (frac f4) = frac f2)
 716           [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f2 Hcut).
 717            rewrite > assoc_Zplus.reflexivity
 718           |rewrite < H3.
 719            generalize in match H2.
 720            cases f2;intro
 721             [change with
 722              (rtimes (rtimes (Z_to_ratio (pos n)) (frac f)) (frac f4)=Z_to_ratio (pos n)).
 723              rewrite > Z_to_ratio_frac_frac.
 724              rewrite > H4.
 725              rewrite > rtimes_oner.
 726              reflexivity
 727             |change with
 728              (rtimes (rtimes (Z_to_ratio (neg n)) (frac f)) (frac f4)=Z_to_ratio (neg n)).
 729              rewrite > Z_to_ratio_frac_frac.
 730              rewrite > H4.
 731              rewrite > rtimes_oner.
 732              reflexivity
 733             |rewrite > H.
 734              rewrite > H4.
 735              rewrite > rtimes_oner.
 736              reflexivity
 737             ]
 738           ]
 739         |elim H2.clear H2.
 740          rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a1 H4).
 741          elim (or_one_frac a f4)
 742           [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 743            cut (rtimes (frac f2) (frac a1) = one)
 744             [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? Hcut).
 745              rewrite > assoc_Zplus.reflexivity
 746             |rewrite < H4.
 747              generalize in match H3.
 748              cases f2;intro
 749               [change with
 750                (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = one).
 751                rewrite < Z_to_ratio_frac_frac.
 752                rewrite > H5.
 753                assumption
 754               |change with
 755                (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = one).
 756                rewrite < Z_to_ratio_frac_frac.
 757                rewrite > H5.
 758                assumption
 759               |rewrite < H.
 760                rewrite > H5.
 761                assumption
 762               ]
 763             ]
 764           |elim H2.clear H2.
 765            rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 H5).
 766            cut (rtimes (frac f2) (frac a1) = frac a2)
 767             [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 Hcut).
 768              rewrite > assoc_Zplus.reflexivity
 769             |rewrite < H4.
 770              generalize in match H3.
 771              cases f2;intro
 772               [change with
 773                (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = frac a2).
 774                rewrite < Z_to_ratio_frac_frac.
 775                rewrite > H2.
 776                assumption
 777               |change with
 778                (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = frac a2).
 779                rewrite < Z_to_ratio_frac_frac.
 780                rewrite > H2.
 781                assumption
 782               |rewrite < H.
 783                rewrite > H2.
 784                assumption
 785               ]
 786             ]
 787           ]
 788         ]
 789       ]
 790     ]
 791   ]
 792 qed.
 793
 794 theorem frac_frac_fracaux: \forall f,f1,f2.
 795 rtimes (rtimes (frac f) (frac f1)) (frac f2)
 796 =rtimes (frac f) (rtimes (frac f1) (frac f2)).
 797 intros.
 798 cases f
 799   [change with
 800    (rtimes (rtimes (Z_to_ratio (pos n)) (frac f1)) (frac f2)
 801     =rtimes (Z_to_ratio (pos n)) (rtimes (frac f1) (frac f2))).
 802    apply Z_to_ratio_frac_frac
 803   |change with
 804    (rtimes (rtimes (Z_to_ratio (neg n)) (frac f1)) (frac f2)
 805     =rtimes (Z_to_ratio (neg n)) (rtimes (frac f1) (frac f2))).
 806    apply Z_to_ratio_frac_frac
 807   |apply cons_frac_frac
 808   ]
 809 qed.
 810
 811 theorem associative_rtimes:associative ? rtimes.
 812 unfold.intros.
 813 cases x
 814   [reflexivity
 815   |cases y
 816     [reflexivity.
 817     |cases z
 818       [rewrite > rtimes_oner.rewrite > rtimes_oner.reflexivity
 819       |apply frac_frac_fracaux
 820       ]
 821     ]
 822   ]
 823 qed.
 824
 825 theorem associative_Qtimes:associative ? Qtimes.
 826 unfold.intros.
 827 cases x
 828   [reflexivity
 829    (* non posso scrivere 2,3: ... ?? *)
 830   |cases y
 831     [reflexivity.
 832     |cases z
 833       [reflexivity
 834       |simplify.rewrite > associative_rtimes.
 835        reflexivity.
 836       |simplify.rewrite > associative_rtimes.
 837        reflexivity
 838       ]
 839     |cases z
 840       [reflexivity
 841       |simplify.rewrite > associative_rtimes.
 842        reflexivity.
 843       |simplify.rewrite > associative_rtimes.
 844        reflexivity
 845       ]
 846     ]
 847   |cases y
 848     [reflexivity.
 849     |cases z
 850       [reflexivity
 851       |simplify.rewrite > associative_rtimes.
 852        reflexivity.
 853       |simplify.rewrite > associative_rtimes.
 854        reflexivity
 855       ]
 856     |cases z
 857       [reflexivity
 858       |simplify.rewrite > associative_rtimes.
 859        reflexivity.
 860       |simplify.rewrite > associative_rtimes.
 861        reflexivity
 862       ]
 863     ]
 864   ]
 865 qed.
 866
 867 theorem Qtimes_OQ: \forall q.Qtimes q OQ = OQ.
 868 intro.cases q;reflexivity.
 869 qed.
 870
 871 theorem symmetric_Qtimes: symmetric ? Qtimes.
 872 unfold.intros.
 873 cases x
 874   [simplify in ⊢ (? ? % ?).rewrite > Qtimes_OQ.reflexivity
 875   |elim y
 876     [reflexivity
 877     |simplify.rewrite > symmetric_rtimes.reflexivity
 878     |simplify.rewrite > symmetric_rtimes.reflexivity
 879     ]
 880   |elim y
 881     [reflexivity
 882     |simplify.rewrite > symmetric_rtimes.reflexivity
 883     |simplify.rewrite > symmetric_rtimes.reflexivity
 884     ]
 885   ]
 886 qed.
 887
 888 theorem Qtimes_Qinv: \forall q. q \neq OQ \to Qtimes q (Qinv q) = Qone.
 889 intro.
 890 cases q;intro
 891   [elim H.reflexivity
 892   |simplify.rewrite > rtimes_rinv.reflexivity
 893   |simplify.rewrite > rtimes_rinv.reflexivity
 894   ]
 895 qed.
 896
 897 theorem eq_Qtimes_OQ_to_eq_OQ: \forall p,q.
 898 Qtimes p q = OQ \to p = OQ \lor q = OQ.
 899 intros 2.
 900 cases p
 901   [intro.left.reflexivity
 902   |cases q
 903     [intro.right.reflexivity
 904     |simplify.intro.destruct H
 905     |simplify.intro.destruct H
 906     ]
 907   |cases q
 908     [intro.right.reflexivity
 909     |simplify.intro.destruct H
 910     |simplify.intro.destruct H
 911     ]
 912   ]
 913 qed.
 914
 915 theorem Qinv_Qtimes: \forall p,q.
 916 p \neq OQ \to q \neq OQ \to
 917 Qinv(Qtimes p q) =
 918 Qtimes (Qinv p) (Qinv q).
 919 intros.
 920 rewrite < Qtimes_Qonel in ⊢ (? ? ? %).
 921 rewrite < (Qtimes_Qinv (Qtimes p q))
 922   [lapply (Qtimes_Qinv ? H).
 923    lapply (Qtimes_Qinv ? H1).
 924    rewrite > symmetric_Qtimes in ⊢ (? ? ? (? % ?)).
 925    rewrite > associative_Qtimes.
 926    rewrite > associative_Qtimes.
 927    rewrite < associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
 928    rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))).
 929    rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
 930    rewrite > Hletin1.
 931    rewrite > Qtimes_Qoner.
 932    rewrite > Hletin.
 933    rewrite > Qtimes_Qoner.
 934    reflexivity
 935   |intro.
 936    elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2)
 937     [apply (H H3)|apply (H1 H3)]
 938   ]
 939 qed.
 940
 941 (* a stronger version, taking advantage of inv(O) = O *)
 942 theorem Qinv_Qtimes': \forall p,q.
 943 Qinv(Qtimes p q) =
 944 Qtimes (Qinv p) (Qinv q).
 945 intros.
 946 cases p
 947   [reflexivity
 948   |cases q
 949     [reflexivity
 950     |apply Qinv_Qtimes;intro;destruct H
 951     |apply Qinv_Qtimes;intro;destruct H
 952     ]
 953   |cases q
 954     [reflexivity
 955     |apply Qinv_Qtimes;intro;destruct H
 956     |apply Qinv_Qtimes;intro;destruct H
 957     ]
 958   ]
 959 qed.
 960
 961 theorem Qtimes_frac_frac: \forall p,q,r,s.
 962 Qtimes (frac p q) (frac r s) = (frac (p*r) (q*s)).
 963 intros.
 964 unfold frac.
 965 rewrite > associative_Qtimes.
 966 rewrite < associative_Qtimes in ⊢ (? ? (? ? %) ?).
 967 rewrite > symmetric_Qtimes in ⊢ (? ? (? ? (? % ?)) ?).
 968 rewrite > associative_Qtimes in ⊢ (? ? (? ? %) ?).
 969 rewrite < associative_Qtimes.
 970 rewrite < times_Qtimes.
 971 rewrite < Qinv_Qtimes'.
 972 rewrite < times_Qtimes.
 973 reflexivity.
 974 qed.
 975
 976
 977 (* la prova seguente e' tutta una ripetizione. Sistemare. *)
 978
 979 theorem Qtimes1: \forall f:fraction.
 980 Qtimes (nat_fact_all_to_Q (numerator f))
 981 (Qinv (nat_fact_all_to_Q (numerator (finv f))))
 982 = Qpos (frac f).
 983 simplify.
 984 intro.elim f
 985   [reflexivity
 986   |reflexivity
 987   |elim (or_numerator_nfa_one_nfa_proper f1)
 988     [elim H1.clear H1.
 989      elim H3.clear H3.
 990      cut (finv (nat_fact_to_fraction a) = f1)
 991       [elim z
 992         [simplify.
 993          rewrite > H2.rewrite > H1.simplify.
 994          rewrite > Hcut.reflexivity
 995         |simplify.
 996          rewrite > H2.rewrite > H1.simplify.
 997          rewrite > Hcut.reflexivity
 998         |simplify.
 999          rewrite > H2.rewrite > H1.simplify.
1000          rewrite > Hcut.reflexivity
1001         ]
1002       |generalize in match H.
1003        rewrite > H2.rewrite > H1.simplify.
1004        intro.destruct H3.assumption
1005       ]
1006     |elim H1.clear H1.
1007      elim z
1008       [simplify.
1009        rewrite > H2.rewrite > H2.simplify.
1010        elim (or_numerator_nfa_one_nfa_proper (finv f1))
1011         [elim H1.clear H1.
1012          rewrite > H3.simplify.
1013          cut (nat_fact_to_fraction a = f1)
1014           [rewrite > Hcut.reflexivity
1015           |generalize in match H.
1016            rewrite > H2.
1017            rewrite > H3.
1018            rewrite > Qtimes_Qoner.
1019            intro.
1020            destruct H1.
1021            assumption
1022           ]
1023         |elim H1.clear H1.
1024          generalize in match H.
1025          rewrite > H2.
1026          rewrite > H3.simplify.
1027          intro.
1028          destruct H1.
1029          rewrite > Hcut.
1030          simplify.reflexivity
1031         ]
1032       |simplify.rewrite > H2.simplify.
1033         elim (or_numerator_nfa_one_nfa_proper (finv f1))
1034         [elim H1.clear H1.
1035          rewrite > H3.simplify.
1036          cut (nat_fact_to_fraction a = f1)
1037           [rewrite > Hcut.reflexivity
1038           |generalize in match H.
1039            rewrite > H2.
1040            rewrite > H3.
1041            rewrite > Qtimes_Qoner.
1042            intro.
1043            destruct H1.
1044            assumption
1045           ]
1046         |elim H1.clear H1.
1047          generalize in match H.
1048          rewrite > H2.
1049          rewrite > H3.simplify.
1050          intro.
1051          destruct H1.
1052          rewrite > Hcut.
1053          simplify.reflexivity
1054         ]
1055       |simplify.rewrite > H2.simplify.
1056         elim (or_numerator_nfa_one_nfa_proper (finv f1))
1057         [elim H1.clear H1.
1058          rewrite > H3.simplify.
1059          cut (nat_fact_to_fraction a = f1)
1060           [rewrite > Hcut.reflexivity
1061           |generalize in match H.
1062            rewrite > H2.
1063            rewrite > H3.
1064            rewrite > Qtimes_Qoner.
1065            intro.
1066            destruct H1.
1067            assumption
1068           ]
1069         |elim H1.clear H1.
1070          generalize in match H.
1071          rewrite > H2.
1072          rewrite > H3.simplify.
1073          intro.
1074          destruct H1.
1075          rewrite > Hcut.
1076          simplify.reflexivity
1077         ]
1078       ]
1079     ]
1080   ]
1081 qed.
1082
1083 (*
1084 definition numQ:Q \to Z \def
1085 \lambda q.
1086 match q with
1087 [OQ \Rightarrow OZ
1088 |Qpos r \Rightarrow Z_of_nat (defactorize (numeratorQ (Qpos r)))
1089 |Qneg r \Rightarrow neg_Z_of_nat (defactorize (numeratorQ (Qpos r)))
1090 ].
1091 *)
1092
1093 definition numQ:Q \to nat \def
1094 \lambda q. defactorize (numeratorQ q).
1095
1096 definition denomQ:Q \to nat \def
1097 \lambda q. defactorize (numeratorQ (Qinv q)).
1098
1099 definition Qopp:Q \to Q \def \lambda q.
1100 match q with
1101 [OQ \Rightarrow OQ
1102 |Qpos q \Rightarrow Qneg q
1103 |Qneg q \Rightarrow Qpos q
1104 ].
1105
1106 theorem frac_numQ_denomQ1: \forall r:ratio.
1107 frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
1108 intro.
1109 unfold frac.unfold denomQ.unfold numQ.
1110 unfold nat_to_Q.
1111 rewrite > factorize_defactorize.
1112 rewrite > factorize_defactorize.
1113 elim r
1114   [reflexivity
1115   |elim f
1116     [reflexivity
1117     |reflexivity
1118     |apply Qtimes1.
1119     ]
1120   ]
1121 qed.
1122
1123 theorem frac_numQ_denomQ2: \forall r:ratio.
1124 frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
1125 intro.
1126 unfold frac.unfold denomQ.unfold numQ.
1127 unfold nat_to_Q.
1128 rewrite > factorize_defactorize.
1129 rewrite > factorize_defactorize.
1130 elim r
1131   [reflexivity
1132   |elim f
1133     [reflexivity
1134     |reflexivity
1135     |apply Qtimes1.
1136     ]
1137   ]
1138 qed.
1139
1140 definition Qabs:Q \to Q \def \lambda q.
1141 match q with
1142 [OQ \Rightarrow OQ
1143 |Qpos q \Rightarrow Qpos q
1144 |Qneg q \Rightarrow Qpos q
1145 ].
1146
1147 theorem frac_numQ_denomQ: \forall q.
1148 frac (numQ q) (denomQ q) = (Qabs q).
1149 intros.
1150 cases q
1151   [reflexivity
1152   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
1153   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
1154   ]
1155 qed.
1156
1157 definition Qfrac: Z \to nat \to Q \def
1158 \lambda z,n.match z with
1159 [OZ \Rightarrow OQ
1160 |Zpos m \Rightarrow (frac (S m) n)
1161 |Zneg m \Rightarrow Qopp (frac (S m) n)
1162 ].
1163
1164 definition QnumZ \def \lambda q.
1165 match q with
1166 [OQ \Rightarrow OZ
1167 |Qpos r \Rightarrow Z_of_nat (numQ (Qpos r))
1168 |Qneg r \Rightarrow neg_Z_of_nat (numQ (Qpos r))
1169 ].
1170
1171 theorem Qfrac_Z_of_nat: \forall n,m.
1172 Qfrac (Z_of_nat n) m = frac n m.
1173 intros.cases n;reflexivity.
1174 qed.
1175
1176 theorem Qfrac_neg_Z_of_nat: \forall n,m.
1177 Qfrac (neg_Z_of_nat n) m = Qopp (frac n m).
1178 intros.cases n;reflexivity.
1179 qed.
1180
1181 theorem Qfrac_QnumZ_denomQ: \forall q.
1182 Qfrac (QnumZ q) (denomQ q) = q.
1183 intros.
1184 cases q
1185   [reflexivity
1186   |change with
1187     (Qfrac (Z_of_nat (numQ (Qpos r))) (denomQ (Qpos r))=Qpos r).
1188    rewrite > Qfrac_Z_of_nat.
1189    apply frac_numQ_denomQ1.
1190   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
1191   ]
1192 qed.
1193