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

[helm.git] / helm / software / matita / contribs / CoRN-Decl / algebra / Cauchy_COF.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma
index f2ee13a4916a58d538f4a2087dd2f53a58bf31a9..46cfc76471e8b0a26114e1fbac536587458c92f9 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma
@@ -16,15 +16,13 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/algebra/Cauchy_COF".
 
+include "CoRN.ma".
+
 (* $Id: Cauchy_COF.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *)
 
-(* INCLUDE
-COrdCauchy
-*)
+include "algebra/COrdCauchy.ma".
 
-(* INCLUDE
-RingReflection
-*)
+include "tactics/RingReflection.ma".
 
 (*#*
 * The Field of Cauchy Sequences
@@ -37,10 +35,10 @@ field [F], we can define a new ordered field of Cauchy sequences over [F].
 *)
 
 (* UNEXPORTED
-Section Structure.
+Section Structure
 *)
 
-inline cic:/CoRN/algebra/Cauchy_COF/F.var.
+inline "cic:/CoRN/algebra/Cauchy_COF/Structure/F.var" "Structure__".
 
 (*#*
 ** Setoid Structure
@@ -52,38 +50,38 @@ onwards [(y n) [-] (x n)] is greater than some fixed, positive
 than the other, equality is the negation of the apartness.
 *)
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_Set.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_Set.con".
 
 (* UNEXPORTED
-Section CSetoid_Structure.
+Section CSetoid_Structure
 *)
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_lt.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_lt.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_ap.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_ap.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_eq.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_eq.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_lt_cotrans.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_lt_cotrans.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_ap_cotrans.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_cotrans.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_ap_symmetric.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_symmetric.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_lt_irreflexive.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_lt_irreflexive.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_ap_irreflexive.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_irreflexive.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_ap_eq_tight.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_eq_tight.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_CSetoid.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_CSetoid.con".
 
 (* UNEXPORTED
-End CSetoid_Structure.
+End CSetoid_Structure
 *)
 
 (* UNEXPORTED
-Section Group_Structure.
+Section Group_Structure
 *)
 
 (*#*
@@ -92,76 +90,76 @@ The group structure is just the expected one; the lemmas which
 are specifically proved are just the necessary ones to get the group axioms.
 *)
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_plus.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_plus.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_zero.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_zero.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_plus_lft_ext.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_plus_lft_ext.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_plus_assoc.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_plus_assoc.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_zero_lft_unit.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_zero_lft_unit.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_plus_comm.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_plus_comm.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_inv.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_inv.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_inv_is_inv.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_inv_is_inv.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_inv_ext.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_inv_ext.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/Rinv.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/Rinv.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_CAbGroup.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_CAbGroup.con".
 
 (* UNEXPORTED
-End Group_Structure.
+End Group_Structure
 *)
 
 (* UNEXPORTED
-Section Ring_Structure.
+Section Ring_Structure
 *)
 
 (*#* ** Ring Structure
 Same comments as previously.
 *)
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_mult.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_mult.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_one.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_one.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_one_ap_zero.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_one_ap_zero.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_plus.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_plus.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_minus.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_minus.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_one_rht_unit.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_one_rht_unit.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_mult_comm.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_comm.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_mult_ap_zero'.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_ap_zero'.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_mult_lft_ext.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_lft_ext.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_mult_rht_ext.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_rht_ext.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_mult_strext.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_strext.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/Rmult.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/Rmult.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_mult_assoc.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_assoc.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_one_lft_unit.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_one_lft_unit.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_CRing.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_CRing.con".
 
 (* UNEXPORTED
-End Ring_Structure.
+End Ring_Structure
 *)
 
 (* UNEXPORTED
-Section Field_Structure.
+Section Field_Structure
 *)
 
 (*#* ** Field Structure
@@ -170,24 +168,24 @@ that our ring is actually an integral domain.  The rest then follows
 quite straightforwardly.
 *)
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_integral_domain.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_integral_domain.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_recip.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_recip.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_recip_strext.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_recip_strext.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse'.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse'.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_CField.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_CField.con".
 
 (* UNEXPORTED
-End Field_Structure.
+End Field_Structure
 *)
 
 (* UNEXPORTED
-Section Order.
+Section Order
 *)
 
 (*#* ** Order Structure
@@ -195,22 +193,22 @@ Finally, we extend the field structure with the ordering we
 defined at the beginning.
 *)
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_lt_strext.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_lt_strext.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/Rlt.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/Rlt.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/Rlt_transitive.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/Rlt_transitive.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/Rlt_strict.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/Rlt_strict.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_plus_resp_lt.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_plus_resp_lt.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_mult_resp_lt.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_resp_lt.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_COrdField.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_COrdField.con".
 
 (* UNEXPORTED
-End Order.
+End Order
 *)
 
 (*#*
@@ -219,28 +217,28 @@ Auxiliary characterizations of the main relations on [R_Set].
 *)
 
 (* UNEXPORTED
-Section Auxiliary.
+Section Auxiliary
 *)
 
-inline cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_1.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_1.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_2.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_2.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_1.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_1.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/Eq_alt_1.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_1.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_2.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_2.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_1.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_1.con".
 
-inline cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_2.con.
+inline "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_2.con".
 
 (* UNEXPORTED
-End Auxiliary.
+End Auxiliary
 *)
 
 (* UNEXPORTED
-End Structure.
+End Structure
 *)