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 \to ratio \to ratio \def
  19 \lambda r,s:ratio.
  20   match r with
  21   [one \Rightarrow s
  22   | (frac f) \Rightarrow
  23       match s with
  24       [one \Rightarrow frac f
  25       | (frac g) \Rightarrow ftimes f g]].
  26
  27 theorem symmetric_rtimes : symmetric ratio rtimes.
  28 change with (\forall 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_rinv: \forall r:ratio. rtimes r (rinv r) = one.
  41 intro.elim r.
  42 reflexivity.
  43 simplify.apply ftimes_finv.
  44 qed.