X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Fratio%2Fratio.ma;h=754b7ad70573e54be565b5dd201d098cc1387664;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=38f2f07b1d51d70ed72abbaf61ea8b05baf03aab;hpb=13ee180b4b982b7a150e8d727ed4b83813ac3fa2;p=helm.git

diff --git a/helm/software/matita/library/Q/ratio/ratio.ma b/helm/software/matita/library/Q/ratio/ratio.ma
index 38f2f07b1..754b7ad70 100644
--- a/helm/software/matita/library/Q/ratio/ratio.ma
+++ b/helm/software/matita/library/Q/ratio/ratio.ma
@@ -17,3 +17,16 @@ include "Q/fraction/fraction.ma".
 inductive ratio : Set \def
       one :  ratio
     | frac : fraction \to ratio.
+
+definition unfrac \def \lambda f.
+match f with
+  [one \Rightarrow pp O
+  |frac f \Rightarrow f
+  ]
+.
+
+lemma injective_frac: injective fraction ratio frac.
+unfold.intros.
+change with ((unfrac (frac x)) = (unfrac (frac y))).
+rewrite < H.reflexivity.
+qed.