X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Fq.ma;h=072532d7bc7a4c8732486f5886a9147f082d5523;hb=063523ae5f8da7e6458232f4afb6744ec86dc8bd;hp=340154979777529f94387cd1c630c6234cf21ab5;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma
index 340154979..072532d7b 100644
--- a/helm/software/matita/library/Q/q.ma
+++ b/helm/software/matita/library/Q/q.ma
@@ -199,9 +199,8 @@ intros.apply (fraction_elim2
   intros.simplify.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
   intros.simplify.unfold Not.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.
   intros.
-   change in match (eqfb (cons x f1) (cons y g1)) 
-   with (andb (eqZb x y) (eqfb f1 g1)).
-    apply eqZb_elim.
+   simplify.
+   apply eqZb_elim.
       intro.generalize in match H.elim (eqfb f1 g1).
         simplify.apply eq_f2.assumption.
         apply H2.
@@ -263,6 +262,7 @@ unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes
   intros.change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)).
    rewrite < sym_Zplus.reflexivity.
   intros.
+   (*CSC: simplify does something nasty here because of a redex in Zplus *)
    change with 
    (match ftimes f g with
    [ one \Rightarrow Z_to_ratio (x1 + y1)
@@ -279,6 +279,7 @@ intro.elim f.
    rewrite > Zplus_Zopp.reflexivity.
   change with (Z_to_ratio (neg n + - (neg n)) = one).
    rewrite > Zplus_Zopp.reflexivity.
+   (*CSC: simplify does something nasty here because of a redex in Zplus *)
 (* again: we would need something to help finding the right change *)
   change with 
   (match ftimes f1 (finv f1) with
@@ -318,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