- new library/logic/coimplication.ma uses new decompose tactic

[helm.git] / helm / software / matita / contribs / CoRN-Decl / transc / InvTrigonom.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/InvTrigonom.ma b/helm/software/matita/contribs/CoRN-Decl/transc/InvTrigonom.ma
index 6ec5b90b431e84595e369da6bfc2f58a7a9a4640..5296d75cb8efe0baeae8b31147530637e66c1474 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/transc/InvTrigonom.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/transc/InvTrigonom.ma
@@ -16,19 +16,15 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/transc/InvTrigonom".
 
+include "CoRN.ma".
+
 (* $Id: InvTrigonom.v,v 1.9 2004/04/23 10:01:07 lcf Exp $ *)
 
-(* INCLUDE
-RealPowers
-*)
+include "transc/RealPowers.ma".
 
-(* INCLUDE
-TrigMon
-*)
+include "transc/TrigMon.ma".
 
-(* INCLUDE
-StrongIVT
-*)
+include "ftc/StrongIVT.ma".
 
 (*#* printing ArcSin %\ensuremath{\arcsin}% *)
 
@@ -55,17 +51,17 @@ Arccosine is defined in terms of arcsine by the relation
 Opaque Sine Cosine Expon Logarithm.
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/ArcSin_def_lemma.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcSin_def_lemma.con".
 
-inline cic:/CoRN/transc/InvTrigonom/ArcSin_def_zero.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcSin_def_zero.con".
 
-inline cic:/CoRN/transc/InvTrigonom/ArcSin.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcSin.con".
 
-inline cic:/CoRN/transc/InvTrigonom/ArcSin_domain.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcSin_domain.con".
 
-inline cic:/CoRN/transc/InvTrigonom/Continuous_ArcSin.con.
+inline "cic:/CoRN/transc/InvTrigonom/Continuous_ArcSin.con".
 
-inline cic:/CoRN/transc/InvTrigonom/Derivative_ArcSin.con.
+inline "cic:/CoRN/transc/InvTrigonom/Derivative_ArcSin.con".
 
 (* UNEXPORTED
 Hint Resolve Derivative_ArcSin: derivate.
@@ -78,28 +74,28 @@ Hint Resolve Continuous_ArcSin: continuous.
 (*#* ***Arccosine
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/ArcCos.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcCos.con".
 
-inline cic:/CoRN/transc/InvTrigonom/ArcCos_domain.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcCos_domain.con".
 
-inline cic:/CoRN/transc/InvTrigonom/Continuous_ArcCos.con.
+inline "cic:/CoRN/transc/InvTrigonom/Continuous_ArcCos.con".
 
-inline cic:/CoRN/transc/InvTrigonom/Derivative_ArcCos.con.
+inline "cic:/CoRN/transc/InvTrigonom/Derivative_ArcCos.con".
 
 (*#* ***Arctangent
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/ArcTan_def_lemma.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcTan_def_lemma.con".
 
-inline cic:/CoRN/transc/InvTrigonom/ArcTang.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcTang.con".
 
-inline cic:/CoRN/transc/InvTrigonom/ArcTan_domain.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcTan_domain.con".
 
-inline cic:/CoRN/transc/InvTrigonom/ArcTan.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcTan.con".
 
-inline cic:/CoRN/transc/InvTrigonom/Continuous_ArcTan.con.
+inline "cic:/CoRN/transc/InvTrigonom/Continuous_ArcTan.con".
 
-inline cic:/CoRN/transc/InvTrigonom/Derivative_ArcTan.con.
+inline "cic:/CoRN/transc/InvTrigonom/Derivative_ArcTan.con".
 
 (* UNEXPORTED
 Hint Resolve Derivative_ArcCos Derivative_ArcTan: derivate.
@@ -110,7 +106,7 @@ Hint Resolve Continuous_ArcCos Continuous_ArcTan: continuous.
 *)
 
 (* UNEXPORTED
-Section Inverses.
+Section Inverses
 *)
 
 (*#* **Composition properties
@@ -120,59 +116,59 @@ We now prove that this functions are in fact inverses to the corresponding trigo
 ***Sine and Arcsine
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/maps_Sin.con.
+inline "cic:/CoRN/transc/InvTrigonom/maps_Sin.con".
 
-inline cic:/CoRN/transc/InvTrigonom/ArcSin_Sin_inv.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcSin_Sin_inv.con".
 
 (* UNEXPORTED
 Opaque ArcSin.
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/ArcSin_Sin.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcSin_Sin.con".
 
 (* UNEXPORTED
 Transparent ArcSin.
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/ArcSin_range.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcSin_range.con".
 
 (* UNEXPORTED
 Transparent ArcSin.
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/Sin_ArcSin.con.
+inline "cic:/CoRN/transc/InvTrigonom/Sin_ArcSin.con".
 
-inline cic:/CoRN/transc/InvTrigonom/Sin_ArcSin_inv.con.
+inline "cic:/CoRN/transc/InvTrigonom/Sin_ArcSin_inv.con".
 
-inline cic:/CoRN/transc/InvTrigonom/ArcSin_resp_leEq.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcSin_resp_leEq.con".
 
 (*#* ***Cosine and Arcosine
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/ArcCos_Cos.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcCos_Cos.con".
 
-inline cic:/CoRN/transc/InvTrigonom/Cos_ArcCos.con.
+inline "cic:/CoRN/transc/InvTrigonom/Cos_ArcCos.con".
 
-inline cic:/CoRN/transc/InvTrigonom/ArcCos_Cos_inv.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcCos_Cos_inv.con".
 
-inline cic:/CoRN/transc/InvTrigonom/Cos_ArcCos_inv.con.
+inline "cic:/CoRN/transc/InvTrigonom/Cos_ArcCos_inv.con".
 
 (* UNEXPORTED
 Opaque ArcSin.
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/ArcCos_resp_leEq.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcCos_resp_leEq.con".
 
 (*#* ***Tangent and Arctangent
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/maps_Tan.con.
+inline "cic:/CoRN/transc/InvTrigonom/maps_Tan.con".
 
 (* UNEXPORTED
 Opaque Tang.
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/ArcTan_Tan_inv.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcTan_Tan_inv.con".
 
 (* UNEXPORTED
 Transparent Tang.
@@ -182,7 +178,7 @@ Transparent Tang.
 Opaque ArcTang.
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/ArcTan_Tan.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcTan_Tan.con".
 
 (* UNEXPORTED
 Opaque iprop.
@@ -196,7 +192,7 @@ Transparent iprop.
 Opaque Cos.
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/Tan_ilim.con.
+inline "cic:/CoRN/transc/InvTrigonom/Tan_ilim.con".
 
 (* UNEXPORTED
 Opaque Min.
@@ -207,68 +203,68 @@ Transparent Cos.
 *)
 
 (* UNEXPORTED
-Section ArcTan_Range.
+Section ArcTan_Range
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/x.var.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/x.var" "Inverses__ArcTan_Range__".
 
 (* begin hide *)
 
-inline cic:/CoRN/transc/InvTrigonom/min.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/max.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/min1.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min1.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/min2.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min2.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/min3.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min3.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/min4.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min4.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/max1.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max1.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/max2.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max2.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/max3.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max3.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/max4.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max4.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/min5.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min5.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/min6.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min6.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/max5.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max5.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/max6.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max6.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/a.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/a1.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a1.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/a2.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a2.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/a3.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a3.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/a4.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a4.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/a5.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a5.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/b.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/b1.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b1.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/b2.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b2.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/b3.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b3.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/b4.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b4.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/b5.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b5.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/ab.con.
+inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/ab.con" "Inverses__ArcTan_Range__".
 
-inline cic:/CoRN/transc/InvTrigonom/ArcTan_range_lemma.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcTan_range_lemma.con".
 
 (* end hide *)
 
@@ -276,25 +272,25 @@ inline cic:/CoRN/transc/InvTrigonom/ArcTan_range_lemma.con.
 Transparent ArcTang.
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/ArcTan_range.con.
+inline "cic:/CoRN/transc/InvTrigonom/ArcTan_range.con".
 
 (* UNEXPORTED
-End ArcTan_Range.
+End ArcTan_Range
 *)
 
 (* UNEXPORTED
 Transparent ArcTang.
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/Tan_ArcTan.con.
+inline "cic:/CoRN/transc/InvTrigonom/Tan_ArcTan.con".
 
 (* UNEXPORTED
 Opaque ArcTang.
 *)
 
-inline cic:/CoRN/transc/InvTrigonom/Tan_ArcTan_inv.con.
+inline "cic:/CoRN/transc/InvTrigonom/Tan_ArcTan_inv.con".
 
 (* UNEXPORTED
-End Inverses.
+End Inverses
 *)