include "Q/q.ma".
+alias id "finv" = "cic:/matita/Q/fraction/finv/finv.con".
theorem denominator_integral_factor_finv:
∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f).
intro;
elim z; simplify; reflexivity]
qed.
+alias id "Qpos" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/2)".
definition is_positive ≝
λq.
match q with
| _ ⇒ False
].
+alias id "Qneg" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/3)".
definition is_negative ≝
λq.
match q with
| _ ⇒ 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]
+ | elim q in H ⊢ %; assumption]
qed.
+*)
\ No newline at end of file