(* *)
(**************************************************************************)
+include "Q/q/q.ma".
include "Q/q.ma".
-
-let rec finv f \def
- match f with
- [ (pp n) \Rightarrow (nn n)
- | (nn n) \Rightarrow (pp n)
- | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
-
-theorem finv_finv: ∀f. finv (finv f) = f.
- intro;
- elim f;
- [1,2: reflexivity
- | simplify;
- rewrite > H;
- rewrite > Zopp_Zopp;
- reflexivity
- ]
-qed.
-
-definition rinv : ratio \to ratio \def
-\lambda r:ratio.
- match r with
- [one \Rightarrow one
- | (frac f) \Rightarrow frac (finv f)].
-
-theorem rinv_rinv: ∀r. rinv (rinv r) = r.
- intro;
- elim r;
- [ reflexivity
- | simplify;
- rewrite > finv_finv;
- reflexivity]
-qed.
-
-definition Qinv : Q → Q ≝
- λp.
- match p with
- [ OQ ⇒ OQ (* arbitrary value *)
- | Qpos r ⇒ Qpos (rinv r)
- | Qneg r ⇒ Qneg (rinv r)
- ].
-
-theorem Qinv_Qinv: ∀q. Qinv (Qinv q) = q.
- intro;
- elim q;
- [ reflexivity
- |*:simplify;
- rewrite > rinv_rinv;
- reflexivity]
-qed.
+include "Q/fraction/finv.ma".
theorem denominator_integral_factor_finv:
∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f).
| _ ⇒ False
].
+(*
theorem is_positive_denominator_Qinv:
∀q. is_positive q → enumerator q = denominator (Qinv q).
intro;
lapply (is_positive_denominator_Qinv (Qinv q));
[ rewrite > Qinv_Qinv in Hletin;
assumption
- | generalize in match H; elim q; assumption]
+ | elim q in H ⊢ %; assumption]
qed.
theorem is_negative_enumerator_Qinv:
lapply (is_negative_denominator_Qinv (Qinv q));
[ rewrite > Qinv_Qinv in Hletin;
assumption
- | generalize in match H; elim q; assumption]
-qed.
\ No newline at end of file
+ | elim q in H ⊢ %; assumption]
+qed.
+*)
\ No newline at end of file