(* *)
(**************************************************************************)
+include "Q/q/q.ma".
include "Q/q.ma".
+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;
assumption
| elim q in H ⊢ %; assumption]
qed.
+*)
\ No newline at end of file