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.
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)
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
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