1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "Q/q/qinv.ma".
16 include "Q/ratio/rtimes.ma".
18 definition Qtimes : Q \to Q \to Q \def
25 |Qpos q1 \Rightarrow Qpos (rtimes p1 q1)
26 |Qneg q1 \Rightarrow Qneg (rtimes p1 q1)
31 |Qpos q1 \Rightarrow Qneg (rtimes p1 q1)
32 |Qneg q1 \Rightarrow Qpos (rtimes p1 q1)
36 interpretation "rational times" 'times x y = (cic:/matita/Q/q/qtimes/Qtimes.con x y).
38 theorem Qtimes_q_OQ: ∀q. q * OQ = OQ.
44 theorem symmetric_Qtimes: symmetric ? Qtimes.
47 [ rewrite > Qtimes_q_OQ; reflexivity
50 try rewrite > sym_rtimes;
55 theorem Qtimes_q_Qone: ∀q.q * Qone = q.
58 |2,3: cases r; reflexivity
62 theorem Qtimes_Qone_q: ∀q.Qone * q = q.
65 |2,3: cases r; reflexivity
69 theorem Qtimes_Qinv: ∀q. q ≠ OQ → q * (Qinv q) = Qpos one.
74 rewrite > rtimes_rinv;