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 theorem denominator_integral_factor_finv:
18 ∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f).
24 elim z; simplify; reflexivity]
27 definition is_positive ≝
34 definition is_negative ≝
41 theorem is_positive_denominator_Qinv:
42 ∀q. is_positive q → enumerator q = denominator (Qinv q).
49 | rewrite > denominator_integral_factor_finv;
53 theorem is_negative_denominator_Qinv:
54 ∀q. is_negative q → enumerator q = -(denominator (Qinv q)).
61 | rewrite > denominator_integral_factor_finv;
63 elim (denominator_integral_fraction (finv f));
66 | generalize in match (lt_O_defactorize_aux (nat_fact_of_integral_fraction a) O);
67 elim (defactorize_aux (nat_fact_of_integral_fraction a) O);
69 [ elim (Not_lt_n_n ? H)
73 theorem is_positive_enumerator_Qinv:
74 ∀q. is_positive q → enumerator (Qinv q) = denominator q.
76 lapply (is_positive_denominator_Qinv (Qinv q));
77 [ rewrite > Qinv_Qinv in Hletin;
79 | generalize in match H; elim q; assumption]
82 theorem is_negative_enumerator_Qinv:
83 ∀q. is_negative q → enumerator (Qinv q) = -(denominator q).
85 lapply (is_negative_denominator_Qinv (Qinv q));
86 [ rewrite > Qinv_Qinv in Hletin;
88 | generalize in match H; elim q; assumption]