| (cons x f) \Rightarrow f].
theorem injective_pp : injective nat fraction pp.
-simplify.intros.
+unfold injective.intros.
change with ((aux (pp x)) = (aux (pp y))).
apply eq_f.assumption.
qed.
theorem injective_nn : injective nat fraction nn.
-simplify.intros.
+unfold injective.intros.
change with ((aux (nn x)) = (aux (nn y))).
apply eq_f.assumption.
qed.
qed.
theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
-intros.simplify. intro.
+intros.unfold Not. intro.
change with match (pp n) with
[ (pp n) \Rightarrow False
| (nn n) \Rightarrow True
theorem not_eq_pp_cons:
\forall n:nat.\forall x:Z. \forall f:fraction.
pp n \neq cons x f.
-intros.simplify. intro.
+intros.unfold Not. intro.
change with match (pp n) with
[ (pp n) \Rightarrow False
| (nn n) \Rightarrow True
theorem not_eq_nn_cons:
\forall n:nat.\forall x:Z. \forall f:fraction.
nn n \neq cons x f.
-intros.simplify. intro.
+intros.unfold Not. intro.
change with match (nn n) with
[ (pp n) \Rightarrow True
| (nn n) \Rightarrow False
theorem decidable_eq_fraction: \forall f,g:fraction.
decidable (f = g).
-intros.simplify.
+intros.unfold decidable.
apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))).
intros.elim g1.
elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
intros.elim g1.
simplify.apply eqb_elim.
intro.simplify.apply eq_f.assumption.
- intro.simplify.intro.apply H.apply injective_pp.assumption.
+ intro.simplify.unfold Not.intro.apply H.apply injective_pp.assumption.
simplify.apply not_eq_pp_nn.
simplify.apply not_eq_pp_cons.
intros.elim g1.
- simplify.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
+ simplify.unfold Not.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
- intro.simplify.intro.apply H.apply injective_nn.assumption.
+ intro.simplify.unfold Not.intro.apply H.apply injective_nn.assumption.
simplify.apply not_eq_nn_cons.
- intros.simplify.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
- intros.simplify.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.
+ intros.simplify.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
+ intros.simplify.unfold Not.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.
intros.
change in match (eqfb (cons x f1) (cons y g1))
with (andb (eqZb x y) (eqfb f1 g1)).
intro.generalize in match H.elim (eqfb f1 g1).
simplify.apply eq_f2.assumption.
apply H2.
- simplify.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
- intro.simplify.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.
+ simplify.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
+ intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.
qed.
let rec finv f \def
| (frac h) \Rightarrow frac (cons (x + y) h)]]].
theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
-simplify. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
+unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
intros.elim g.
change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)).
apply eq_f.apply sym_Zplus.