+
+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.