1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
17 alias id "finv" = "cic:/matita/Q/fraction/finv/finv.con".
18 theorem denominator_integral_factor_finv:
19 ∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f).
25 elim z; simplify; reflexivity]
28 alias id "Qpos" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/2)".
29 definition is_positive ≝
36 alias id "Qneg" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/3)".
37 definition is_negative ≝
45 theorem is_positive_denominator_Qinv:
46 ∀q. is_positive q → enumerator q = denominator (Qinv q).
53 | rewrite > denominator_integral_factor_finv;
57 theorem is_negative_denominator_Qinv:
58 ∀q. is_negative q → enumerator q = -(denominator (Qinv q)).
65 | rewrite > denominator_integral_factor_finv;
67 elim (denominator_integral_fraction (finv f));
70 | generalize in match (lt_O_defactorize_aux (nat_fact_of_integral_fraction a) O);
71 elim (defactorize_aux (nat_fact_of_integral_fraction a) O);
73 [ elim (Not_lt_n_n ? H)
77 theorem is_positive_enumerator_Qinv:
78 ∀q. is_positive q → enumerator (Qinv q) = denominator q.
80 lapply (is_positive_denominator_Qinv (Qinv q));
81 [ rewrite > Qinv_Qinv in Hletin;
83 | elim q in H ⊢ %; assumption]
86 theorem is_negative_enumerator_Qinv:
87 ∀q. is_negative q → enumerator (Qinv q) = -(denominator q).
89 lapply (is_negative_denominator_Qinv (Qinv q));
90 [ rewrite > Qinv_Qinv in Hletin;
92 | elim q in H ⊢ %; assumption]