few more files, one diverges

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

diff --git a/helm/software/matita/library/Q/ratio/ratio.ma b/helm/software/matita/library/Q/ratio/ratio.ma
index 38f2f07b1d51d70ed72abbaf61ea8b05baf03aab..754b7ad70573e54be565b5dd201d098cc1387664 100644 (file)
--- 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.