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))].
-
-definition rinv : ratio \to ratio \def
-\lambda r:ratio.
- match r with
- [one \Rightarrow one
- | (frac f) \Rightarrow frac (finv f)].
-
-definition Qinv : Q → Q ≝
- λp.
- match p with
- [ OQ ⇒ OQ (* arbitrary value *)
- | Qpos r ⇒ Qpos (rinv r)
- | Qneg r ⇒ Qneg (rinv r)
+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 f;
+ [1,2: reflexivity
+ |simplify;
+ rewrite > H;
+ 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
+ [ Qpos _ ⇒ True
+ | _ ⇒ False
+ ].
+
+alias id "Qneg" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/3)".
+definition is_negative ≝
+ λq.
+ match q with
+ [ Qneg _ ⇒ True
+ | _ ⇒ False
].
+
+(*
+theorem is_positive_denominator_Qinv:
+ ∀q. is_positive q → enumerator q = denominator (Qinv q).
+ intro;
+ elim q;
+ [1,3: elim H;
+ | simplify; clear H;
+ elim r; simplify;
+ [ reflexivity
+ | rewrite > denominator_integral_factor_finv;
+ reflexivity]]
+qed.
+
+theorem is_negative_denominator_Qinv:
+ ∀q. is_negative q → enumerator q = -(denominator (Qinv q)).
+ intro;
+ elim q;
+ [1,2: elim H;
+ | simplify; clear H;
+ elim r; simplify;
+ [ reflexivity
+ | rewrite > denominator_integral_factor_finv;
+ unfold Zopp;
+ elim (denominator_integral_fraction (finv f));
+ simplify;
+ [ reflexivity
+ | generalize in match (lt_O_defactorize_aux (nat_fact_of_integral_fraction a) O);
+ elim (defactorize_aux (nat_fact_of_integral_fraction a) O);
+ simplify;
+ [ elim (Not_lt_n_n ? H)
+ | reflexivity]]]]
+qed.
+
+theorem is_positive_enumerator_Qinv:
+ ∀q. is_positive q → enumerator (Qinv q) = denominator q.
+ intros;
+ lapply (is_positive_denominator_Qinv (Qinv q));
+ [ rewrite > Qinv_Qinv in Hletin;
+ assumption
+ | elim q in H ⊢ %; assumption]
+qed.
+
+theorem is_negative_enumerator_Qinv:
+ ∀q. is_negative q → enumerator (Qinv q) = -(denominator q).
+ intros;
+ lapply (is_negative_denominator_Qinv (Qinv q));
+ [ rewrite > Qinv_Qinv in Hletin;
+ assumption
+ | elim q in H ⊢ %; assumption]
+qed.
+*)
\ No newline at end of file