X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Fratio%2Frtimes.ma;h=a8255afef85d43f274e15979cd1dd8aa2a9ccb43;hb=02e8b3eb9d2a8a3bb3942c41b47b6ac048efd5be;hp=3c7859dbedcdee7c29a615863be077c4190b24ab;hpb=bb6f711dd0c8378d27118b73981515aff05f5750;p=helm.git

diff --git a/helm/software/matita/library/Q/ratio/rtimes.ma b/helm/software/matita/library/Q/ratio/rtimes.ma
index 3c7859dbe..a8255afef 100644
--- a/helm/software/matita/library/Q/ratio/rtimes.ma
+++ b/helm/software/matita/library/Q/ratio/rtimes.ma
@@ -443,3 +443,18 @@ intro.elim r.
 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