apply eq_f.assumption.
qed.
-theorem not_eq_pp_nn: \forall n,m:nat. \lnot (pp n) = (nn m).
+theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
intros.simplify. intro.
change with match (pp n) with
[ (pp n) \Rightarrow False
theorem not_eq_pp_cons:
\forall n:nat.\forall x:Z. \forall f:fraction.
-\lnot (pp n) = (cons x f).
+pp n \neq cons x f.
intros.simplify. intro.
change with match (pp n) with
[ (pp n) \Rightarrow False
theorem not_eq_nn_cons:
\forall n:nat.\forall x:Z. \forall f:fraction.
-\lnot (nn n) = (cons x f).
+nn n \neq cons x f.
intros.simplify. intro.
change with match (nn n) with
[ (pp n) \Rightarrow True
theorem eqfb_to_Prop: \forall f,g:fraction.
match (eqfb f g) with
[true \Rightarrow f=g
-|false \Rightarrow \lnot f=g].
+|false \Rightarrow f \neq g].
intros.apply fraction_elim2
(\lambda f,g.match (eqfb f g) with
[true \Rightarrow f=g
-|false \Rightarrow \lnot f=g]).
+|false \Rightarrow f \neq g]).
intros.elim g1.
simplify.apply eqb_elim.
intro.simplify.apply eq_f.assumption.