-simplify. intros.
-apply fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f).
-intros.elim g.
-change with Z_to_ratio (Zplus (pos n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (pos n)).
-apply eq_f.apply sym_Zplus.
-change with frac (cons (Zplus (pos n) z) f) = frac (cons (Zplus z (pos n)) f).
-rewrite < sym_Zplus.reflexivity.
-change with Z_to_ratio (Zplus (pos n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (pos n)).
-apply eq_f.apply sym_Zplus.
-intros.elim g.
-change with Z_to_ratio (Zplus (neg n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (neg n)).
-apply eq_f.apply sym_Zplus.
-change with frac (cons (Zplus (neg n) z) f) = frac (cons (Zplus z (neg n)) f).
-rewrite < sym_Zplus.reflexivity.
-change with Z_to_ratio (Zplus (neg n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (neg n)).
-apply eq_f.apply sym_Zplus.
-intros.
-change with frac (cons (Zplus x1 (pos m)) f) = frac (cons (Zplus (pos m) x1) f).
-rewrite < sym_Zplus.reflexivity.
-intros.
-change with frac (cons (Zplus x1 (neg m)) f) = frac (cons (Zplus (neg m) x1) f).
-rewrite < sym_Zplus.reflexivity.
-intros.
-change with
- match ftimes f g with
- [ one \Rightarrow Z_to_ratio (Zplus x1 y1)
- | (frac h) \Rightarrow frac (cons (Zplus x1 y1) h)] =
- match ftimes g f with
- [ one \Rightarrow Z_to_ratio (Zplus y1 x1)
- | (frac h) \Rightarrow frac (cons (Zplus y1 x1) h)].
-rewrite < H.rewrite < sym_Zplus.
-reflexivity.
+unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
+ intros.elim g.
+ change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)).
+ apply eq_f.apply sym_Zplus.
+ change with (Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n)).
+ apply eq_f.apply sym_Zplus.
+ change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)).
+ rewrite < sym_Zplus.reflexivity.
+ intros.elim g.
+ change with (Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n)).
+ apply eq_f.apply sym_Zplus.
+ change with (Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n)).
+ apply eq_f.apply sym_Zplus.
+ change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)).
+ rewrite < sym_Zplus.reflexivity.
+ intros.change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)).
+ rewrite < sym_Zplus.reflexivity.
+ intros.change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)).
+ rewrite < sym_Zplus.reflexivity.
+ intros.
+ change with
+ (match ftimes f g with
+ [ one \Rightarrow Z_to_ratio (x1 + y1)
+ | (frac h) \Rightarrow frac (cons (x1 + y1) h)] =
+ match ftimes g f with
+ [ one \Rightarrow Z_to_ratio (y1 + x1)
+ | (frac h) \Rightarrow frac (cons (y1 + x1) h)]).
+ rewrite < H.rewrite < sym_Zplus.reflexivity.