X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Fq.ma;h=072532d7bc7a4c8732486f5886a9147f082d5523;hb=04d8e2282a3536a9b822a8dbfcbdb4e3a949f04d;hp=07a992926f1a434d5f01fc20f1873f27a3da3963;hpb=ebb14e0084aecd167bc42245625c4eb3167df9d5;p=helm.git

diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma
index 07a992926..072532d7b 100644
--- a/helm/software/matita/library/Q/q.ma
+++ b/helm/software/matita/library/Q/q.ma
@@ -319,3 +319,23 @@ intro.elim r.
 reflexivity.
 simplify.apply ftimes_finv.
 qed.
+
+definition Qtimes : Q \to Q \to Q \def
+\lambda p,q.
+  match p with
+  [OQ \Rightarrow OQ
+  |Qpos p1 \Rightarrow 
+    match q with
+    [OQ \Rightarrow OQ
+    |Qpos q1 \Rightarrow Qpos (rtimes p1 q1)
+    |Qneg q1 \Rightarrow Qneg (rtimes p1 q1)
+    ]
+  |Qneg p1 \Rightarrow 
+    match q with
+    [OQ \Rightarrow OQ
+    |Qpos q1 \Rightarrow Qneg (rtimes p1 q1)
+    |Qneg q1 \Rightarrow Qpos (rtimes p1 q1)
+    ]
+  ]
+.
+    
\ No newline at end of file