Even more Q stuff classified.

[helm.git] / helm / software / matita / library / Q / ratio / rtimes.ma

diff --git a/helm/software/matita/library/Q/ratio/rtimes.ma b/helm/software/matita/library/Q/ratio/rtimes.ma
index 3c7859dbedcdee7c29a615863be077c4190b24ab..a8255afef85d43f274e15979cd1dd8aa2a9ccb43 100644 (file)
--- 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