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.