notation factored, coercion commant taking terms and not only URI

[helm.git] / helm / software / matita / library / Q / inv.ma

diff --git a/helm/software/matita/library/Q/inv.ma b/helm/software/matita/library/Q/inv.ma
index 8c6f1db95ecffd4d98e08768f28fc04564a1c92e..9cc2fc3b43ea9c7c06fd001338221d0c38d37759 100644 (file)
--- a/helm/software/matita/library/Q/inv.ma
+++ b/helm/software/matita/library/Q/inv.ma
@@ -14,6 +14,7 @@
 
 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;
@@ -24,6 +25,7 @@ theorem denominator_integral_factor_finv:
    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
@@ -31,6 +33,7 @@ definition is_positive ≝
    | _ ⇒ False
    ].
 
+alias id "Qneg" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/3)".
 definition is_negative ≝
  λq.
   match q with
@@ -38,6 +41,7 @@ definition is_negative ≝
    | _ ⇒ False
    ].
 
+(*
 theorem is_positive_denominator_Qinv:
  ∀q. is_positive q → enumerator q = denominator (Qinv q).
  intro;
@@ -76,7 +80,7 @@ theorem is_positive_enumerator_Qinv:
  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:
@@ -85,5 +89,6 @@ 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