set "baseuri" "cic:/matita/CoRN-Decl/CoRN".
+include "preamble.ma".
+
(* From algebra/Basics ****************************************************)
(* NOTATION
Notation Proj2 := (proj2 (B:=_)).
*)
-(* COERCION
-Z_of_nat
-*)
+coercion cic:/Coq/ZArith/BinInt/Z_of_nat.con 0 (* compounds *).
(* From algebra/CAbGroups *************************************************)
-(* COERCION
-cag_crr
-*)
+coercion cic:/CoRN/algebra/CAbGroups/cag_crr.con 0 (* compounds *).
(* From algebra/CAbMonoids ************************************************)
-(* COERCION
-cam_crr
-*)
+coercion cic:/CoRN/algebra/CAbMonoids/cam_crr.con 0 (* compounds *).
(* From algebra/CFields ***************************************************)
-(* COERCION
-cf_crr
-*)
+coercion cic:/CoRN/algebra/CFields/cf_crr.con 0 (* compounds *).
(* NOTATION
Notation "x [/] y [//] Hy" := (cf_div x y Hy) (at level 80).
(* From algebra/CGroups ***************************************************)
-(* COERCION
-cg_crr
-*)
+coercion cic:/CoRN/algebra/CGroups/cg_crr.con 0 (* compounds *).
(* NOTATION
Notation "[--] x" := (cg_inv x) (at level 2, right associativity).
(* From algebra/CMonoids **************************************************)
-(* COERCION
-cm_crr
-*)
+coercion cic:/CoRN/algebra/CMonoids/cm_crr.con 0 (* compounds *).
(* NOTATION
Notation Zero := (cm_unit _).
(* From algebra/COrdCauchy ************************************************)
-(* COERCION
-CS_seq
-*)
+coercion cic:/CoRN/algebra/COrdCauchy/CS_seq.con 0 (* compounds *).
(* From algebra/COrdFields ************************************************)
-(* COERCION
-cof_crr
-*)
+coercion cic:/CoRN/algebra/COrdFields/cof_crr.con 0 (* compounds *).
(* NOTATION
Infix "[<]" := cof_less (at level 70, no associativity).
(* From algebra/CRings ****************************************************)
-(* COERCION
-cr_crr
-*)
+coercion cic:/CoRN/algebra/CRings/cr_crr.con 0 (* compounds *).
(* NOTATION
Notation One := (cr_one _).
(* From algebra/CSemiGroups ***********************************************)
-(* COERCION
-csg_crr
-*)
+coercion cic:/CoRN/algebra/CSemiGroups/csg_crr.con 0 (* compounds *).
(* NOTATION
Infix "[+]" := csg_op (at level 50, left associativity).
Notation Conj := (conjP _).
*)
-(* COERCION
-bpfpfun
-*)
+coercion cic:/CoRN/algebra/CSetoidFun/bpfpfun.con 0 (* compounds *).
(* NOTATION
Notation BDom := (bpfdom _ _).
*)
-(* COERCION
-pfpfun
-*)
+coercion cic:/CoRN/algebra/CSetoidFun/pfpfun.con 0 (* compounds *).
(* NOTATION
Notation Dom := (pfdom _).
(* From algebra/CSetoids **************************************************)
-(* COERCION
-cs_crr
-*)
+coercion cic:/CoRN/algebra/CSetoids/cs_crr.con 0 (* compounds *).
(* NOTATION
Infix "[=]" := cs_eq (at level 70, no associativity).
Infix "[~=]" := cs_neq (at level 70, no associativity).
*)
-(* COERCION
-csp_pred
-*)
+coercion cic:/CoRN/algebra/CSetoids/csp_pred.con 0 (* compounds *).
-(* COERCION
-csp'_pred
-*)
+coercion cic:/CoRN/algebra/CSetoids/csp'_pred.con 0 (* compounds *).
-(* COERCION
-csr_rel
-*)
+coercion cic:/CoRN/algebra/CSetoids/csr_rel.con 0 (* compounds *).
-(* COERCION
-Ccsr_rel
-*)
+coercion cic:/CoRN/algebra/CSetoids/Ccsr_rel.con 0 (* compounds *).
-(* COERCION
-csf_fun
-*)
+coercion cic:/CoRN/algebra/CSetoids/csf_fun.con 0 (* compounds *).
-(* COERCION
-csbf_fun
-*)
+coercion cic:/CoRN/algebra/CSetoids/csbf_fun.con 0 (* compounds *).
-(* COERCION
-un_op_fun
-*)
+coercion cic:/CoRN/algebra/CSetoids/un_op_fun.con 0 (* compounds *).
-(* COERCION
-bin_op_bin_fun
-*)
+coercion cic:/CoRN/algebra/CSetoids/bin_op_bin_fun.con 0 (* compounds *).
-(* COERCION
-outer_op_bin_fun
-*)
+coercion cic:/CoRN/algebra/CSetoids/outer_op_bin_fun.con 0 (* compounds *).
-(* COERCION
-scs_elem
-*)
+coercion cic:/CoRN/algebra/CSetoids/scs_elem.con 0 (* compounds *).
(* From algebra/CVectorSpace **********************************************)
-(* COERCION
-vs_vs
-*)
+coercion cic:/CoRN/algebra/CVectorSpace/vs_vs.con 0 (* compounds *).
(* NOTATION
Infix "[']" := vs_op (at level 30, no associativity).
(* From fta/CC_Props ******************************************************)
-(* COERCION
-CC_seq
-*)
+coercion cic:/CoRN/fta/CC_Props/CC_seq.con 0 (* compounds *).
(* From fta/FTAreg ********************************************************)
-(* COERCION
-z_el
-*)
+coercion cic:/CoRN/fta/FTAreg/z_el.con 0 (* compounds *).
-(* COERCION
-Kntup
-*)
+coercion cic:/CoRN/fta/FTAreg/Kntup.con 0 (* compounds *).
(* From ftc/FTC ***********************************************************)
(* From ftc/MoreIntervals *************************************************)
-(* COERCION
-iprop
-*)
+coercion cic:/CoRN/ftc/MoreIntervals/iprop.con 0 (* compounds *).
(* From ftc/Partitions ****************************************************)
-(* COERCION
-Pts
-*)
+coercion cic:/CoRN/ftc/Partitions/Pts.con 0 (* compounds *).
(* From ftc/RefLemma ******************************************************)
(* From metrics/CMetricSpaces *********************************************)
-(* COERCION
-scms_crr
-*)
+coercion cic:/CoRN/metrics/CMetricSpaces/scms_crr.con 0 (* compounds *).
(* From metrics/CPseudoMSpaces ********************************************)
-(* COERCION
-cms_crr
-*)
+coercion cic:/CoRN/metrics/CPseudoMSpaces/cms_crr.con 0 (* compounds *).
(* NOTATION
Infix "[-d]" := cms_d (at level 68, left associativity).
Notation "{-Q}" := Qopp (at level 1, left associativity).
*)
-(* COERCION
-inject_Z
-*)
+coercion cic:/CoRN/model/structures/Qsec/inject_Z.con 0 (* compounds *).
(* From model/structures/Zsec *********************************************)
Infix "{#Z}" := ap_Z (no associativity, at level 90).
*)
-(* COERCION
-Zpos
-*)
+coercion cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2) 0 (* compounds *).
(* From reals/Bridges_LUB *************************************************)
(* From reals/CMetricFields ***********************************************)
-(* COERCION
-cmf_crr
-*)
+coercion cic:/CoRN/reals/CMetricFields/cmf_crr.con 0 (* compounds *).
(* NOTATION
Notation MAbs := (cmf_abs _).
*)
-(* COERCION
-MCS_seq
-*)
+coercion cic:/CoRN/reals/CMetricFields/MCS_seq.con 0 (* compounds *).
(* From reals/CReals ******************************************************)
-(* COERCION
-crl_crr
-*)
+coercion cic:/CoRN/reals/CReals/crl_crr.con 0 (* compounds *).
(* From reals/CauchySeq ***************************************************)
(* From reals/Q_dense *****************************************************)
-(* COERCION
-pair_crr
-*)
+coercion cic:/CoRN/reals/Q_dense/pair_crr.con 0 (* compounds *).
(* NOTATION
Notation "( A , B )" := (pairT A B).
(* From reals/Q_in_CReals *************************************************)
-(* COERCION
-nat_of_P
-*)
+coercion cic:/Coq/NArith/BinPos/nat_of_P.con 0 (* compounds *).
(* From reals/R_morphism **************************************************)
-(* COERCION
-map
-*)
+coercion cic:/CoRN/reals/R_morphism/map.con 0 (* compounds *).
(* From tactics/FieldReflection *******************************************)
(* From devel/loeb/per/lst2fun ********************************************)
-(* COERCION
-F_crr
-*)
+coercion cic:/CoRN/devel/loeb/per/lst2fun/F_crr.con 0 (* compounds *).
-(* COERCION
-to_nat
-*)
+coercion cic:/CoRN/devel/loeb/per/lst2fun/to_nat.con 0 (* compounds *).