reflexivity.
simplify.apply ftimes_finv.
qed.
+
+theorem rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
+(rtimes (frac f) (frac g) = one \land
+ rtimes (frac (cons x f)) (frac (cons y g)) = nat_frac_item_to_ratio (x + y))
+\lor (\exists h.rtimes (frac f) (frac g) = frac h \land
+rtimes (frac (cons x f)) (frac (cons y g)) =
+frac (cons (x + y) h)).
+intros.
+simplify.
+elim (rtimes (frac f) (frac g));simplify
+ [left.split;reflexivity
+ |right.
+ apply (ex_intro ? ? f1).
+ split;reflexivity]
+qed.
\ No newline at end of file