More Q stuff organized in a coherent way.

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

diff --git a/helm/software/matita/library/Q/q/qtimes.ma b/helm/software/matita/library/Q/q/qtimes.ma
index 8a94d2b3543d04e3f9bfff6a808d453099f10ecd..e288ef412c4732badb25cee471c2952d75e96e6d 100644 (file)
--- a/helm/software/matita/library/Q/q/qtimes.ma
+++ b/helm/software/matita/library/Q/q/qtimes.ma
@@ -39,7 +39,7 @@ theorem Qtimes_q_OQ: ∀q. q * OQ = OQ.
  intro;
  elim q;
  reflexivity.
-qed. 
+qed.
 
 theorem symmetric_Qtimes: symmetric ? Qtimes.
  intros 2;
@@ -52,6 +52,20 @@ theorem symmetric_Qtimes: symmetric ? Qtimes.
   ]
 qed.
 
+theorem Qtimes_q_Qone: ∀q.q * Qone = q.
+ intro.cases q
+  [reflexivity
+  |2,3: cases r; reflexivity
+  ]
+qed.
+
+theorem Qtimes_Qone_q: ∀q.Qone * q = q.
+ intro.cases q
+  [reflexivity
+  |2,3: cases r; reflexivity
+  ]
+qed.
+
 theorem Qtimes_Qinv: ∀q. q ≠ OQ → q * (Qinv q) = Qpos one.
  intro;
  elim q;