Some axioms for Q.

[helm.git] / matita / library / Q / q.ma

diff --git a/matita/library/Q/q.ma b/matita/library/Q/q.ma
index 07a992926f1a434d5f01fc20f1873f27a3da3963..23ef525519b42282aa10185e14604e3a12fa8fcc 100644 (file)
--- a/matita/library/Q/q.ma
+++ b/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)
+    ]
+  |neg 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