Even more Q stuff classified.

[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 e288ef412c4732badb25cee471c2952d75e96e6d..52246e5a57794a159c34d7445c3f0cd6c9c114b8 100644 (file)
--- a/helm/software/matita/library/Q/q/qtimes.ma
+++ b/helm/software/matita/library/Q/q/qtimes.ma
@@ -75,3 +75,117 @@ theorem Qtimes_Qinv: ∀q. q ≠ OQ → q * (Qinv q) = Qpos one.
      reflexivity
   ]
 qed.
+
+theorem times_fa_Qtimes: \forall f,g. nat_fact_all_to_Q (times_fa f g) =
+Qtimes (nat_fact_all_to_Q f) (nat_fact_all_to_Q g).
+intros.
+cases f;simplify
+  [reflexivity
+  |cases g;reflexivity
+  |cases g;simplify
+    [reflexivity
+    |reflexivity
+    |rewrite > times_f_ftimes.reflexivity]]
+qed.
+
+theorem times_Qtimes: \forall p,q.
+(nat_to_Q (p*q)) = Qtimes (nat_to_Q p) (nat_to_Q q).
+intros.unfold nat_to_Q.
+rewrite < times_fa_Qtimes.
+rewrite < eq_times_times_fa.
+reflexivity.
+qed.
+
+theorem associative_Qtimes:associative ? Qtimes.
+unfold.intros.
+cases x
+  [reflexivity
+   (* non posso scrivere 2,3: ... ?? *)
+  |cases y
+    [reflexivity.
+    |cases z
+      [reflexivity
+      |simplify.rewrite > associative_rtimes.
+       reflexivity.
+      |simplify.rewrite > associative_rtimes.
+       reflexivity
+      ]
+    |cases z
+      [reflexivity
+      |simplify.rewrite > associative_rtimes.
+       reflexivity.
+      |simplify.rewrite > associative_rtimes.
+       reflexivity
+      ]
+    ]
+  |cases y
+    [reflexivity.
+    |cases z
+      [reflexivity
+      |simplify.rewrite > associative_rtimes.
+       reflexivity.
+      |simplify.rewrite > associative_rtimes.
+       reflexivity
+      ]
+    |cases z
+      [reflexivity
+      |simplify.rewrite > associative_rtimes.
+       reflexivity.
+      |simplify.rewrite > associative_rtimes.
+       reflexivity]]]
+qed.
+
+theorem eq_Qtimes_OQ_to_eq_OQ: \forall p,q.
+Qtimes p q = OQ \to p = OQ \lor q = OQ.
+intros 2.
+cases p
+  [intro.left.reflexivity
+  |cases q
+    [intro.right.reflexivity
+    |simplify.intro.destruct H
+    |simplify.intro.destruct H
+    ]
+  |cases q
+    [intro.right.reflexivity
+    |simplify.intro.destruct H
+    |simplify.intro.destruct H]]
+qed.
+
+theorem Qinv_Qtimes: \forall p,q.
+p \neq OQ \to q \neq OQ \to Qinv(Qtimes p q) = Qtimes (Qinv p) (Qinv q).
+intros.
+rewrite < Qtimes_Qone_q in ⊢ (? ? ? %).
+rewrite < (Qtimes_Qinv (Qtimes p q))
+  [lapply (Qtimes_Qinv ? H).
+   lapply (Qtimes_Qinv ? H1).
+   rewrite > symmetric_Qtimes in ⊢ (? ? ? (? % ?)).
+   rewrite > associative_Qtimes.
+   rewrite > associative_Qtimes.
+   rewrite < associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
+   rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))).
+   rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
+   rewrite > Hletin1.
+   rewrite > Qtimes_q_Qone.
+   rewrite > Hletin.
+   rewrite > Qtimes_q_Qone.
+   reflexivity
+  |intro.
+   elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2)
+    [apply (H H3)|apply (H1 H3)]]
+qed.
+
+(* a stronger version, taking advantage of inv(O) = O *)
+theorem Qinv_Qtimes': \forall p,q. Qinv(Qtimes p q) = Qtimes (Qinv p) (Qinv q).
+intros.
+cases p
+  [reflexivity
+  |cases q
+    [reflexivity
+    |apply Qinv_Qtimes;intro;destruct H
+    |apply Qinv_Qtimes;intro;destruct H
+    ]
+  |cases q
+    [reflexivity
+    |apply Qinv_Qtimes;intro;destruct H
+    |apply Qinv_Qtimes;intro;destruct H]]
+qed.