1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "preamble.ma".
19 (* From algebra/Basics ****************************************************)
22 Notation Pair := (pair (B:=_)).
26 Notation Proj1 := (proj1 (B:=_)).
30 Notation Proj2 := (proj2 (B:=_)).
34 cic:/Coq/ZArith/BinInt/Z_of_nat.con
37 (* From algebra/CAbGroups *************************************************)
40 cic:/CoRN/algebra/CAbGroups/cag_crr.con
43 (* From algebra/CAbMonoids ************************************************)
46 cic:/CoRN/algebra/CAbMonoids/cam_crr.con
49 (* From algebra/CFields ***************************************************)
52 cic:/CoRN/algebra/CFields/cf_crr.con
56 Notation "x [/] y [//] Hy" := (cf_div x y Hy) (at level 80).
60 Notation "{1/} x" := (Frecip x) (at level 2, right associativity).
64 Infix "{/}" := Fdiv (at level 41, no associativity).
67 (* From algebra/CGroups ***************************************************)
70 cic:/CoRN/algebra/CGroups/cg_crr.con
74 Notation "[--] x" := (cg_inv x) (at level 2, right associativity).
78 Infix "[-]" := cg_minus (at level 50, left associativity).
82 Notation "{--} x" := (Finv x) (at level 2, right associativity).
86 Infix "{-}" := Fminus (at level 50, left associativity).
89 (* From algebra/CLogic ****************************************************)
92 Infix "IFF" := Iff (at level 60, right associativity).
96 Infix "or" := COr (at level 85, right associativity).
100 Infix "and" := CAnd (at level 80, right associativity).
104 Notation "{ x : A | P }" := (sigT (fun x : A => P):CProp)
105 (at level 0, x at level 99) : type_scope.
109 Notation "{ x : A | P | Q }" :=
110 (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) :
115 Notation ProjT1 := (proj1_sigT _ _).
119 Notation ProjT2 := (proj2_sigT _ _).
122 (* From algebra/CMonoids **************************************************)
125 cic:/CoRN/algebra/CMonoids/cm_crr.con
129 Notation Zero := (cm_unit _).
132 (* From algebra/COrdAbs ***************************************************)
135 Notation ZeroR := (Zero:R).
139 Notation AbsBig := (absBig _).
142 (* From algebra/COrdCauchy ************************************************)
145 cic:/CoRN/algebra/COrdCauchy/CS_seq.con
148 (* From algebra/COrdFields ************************************************)
151 cic:/CoRN/algebra/COrdFields/cof_crr.con
155 Infix "[<]" := cof_less (at level 70, no associativity).
159 Infix "[>]" := greater (at level 70, no associativity).
163 Infix "[<=]" := leEq (at level 70, no associativity).
167 Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20).
171 Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20).
175 Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20).
179 Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20).
183 Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20).
187 Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20).
191 Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20).
195 Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20).
199 Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20).
203 Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20).
207 Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20).
211 Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20).
214 (* From algebra/COrdFields2 ***********************************************)
217 Notation ZeroR := (Zero:R).
221 Notation OneR := (One:R).
224 (* From algebra/CPoly_ApZero **********************************************)
227 Notation RX := (cpoly_cring R).
231 Notation RX := (cpoly_cring R).
235 Notation RX := (cpoly_cring R).
238 (* From algebra/CPoly_Degree **********************************************)
241 Notation RX := (cpoly_cring R).
245 Notation RX := (cpoly_cring R).
249 Notation FX := (cpoly_cring F).
252 (* From algebra/CPoly_NthCoeff ********************************************)
255 Notation RX := (cpoly_cring R).
259 Notation RX := (cpoly_cring R).
262 (* From algebra/CPolynomials **********************************************)
265 Infix "[+X*]" := cpoly_linear_fun' (at level 50, left associativity).
269 Notation RX := (cpoly_cring CR).
273 Infix "!" := cpoly_apply_fun (at level 1, no associativity).
277 Notation RX := (cpoly_cring R).
281 Notation Cpoly := (cpoly CR).
285 Notation Cpoly_zero := (cpoly_zero CR).
289 Notation Cpoly_linear := (cpoly_linear CR).
293 Notation Cpoly_cring := (cpoly_cring CR).
296 (* From algebra/CRings ****************************************************)
299 cic:/CoRN/algebra/CRings/cr_crr.con
303 Notation One := (cr_one _).
307 Infix "[*]" := cr_mult (at level 40, left associativity).
311 Notation "x [^] n" := (nexp_op _ n x) (at level 20).
315 Notation Two := (nring 2).
319 Notation Three := (nring 3).
323 Notation Four := (nring 4).
327 Notation Six := (nring 6).
331 Notation Eight := (nring 8).
335 Notation Twelve := (nring 12).
339 Notation Sixteen := (nring 16).
343 Notation Nine := (nring 9).
347 Notation Eighteen := (nring 18).
351 Notation TwentyFour := (nring 24).
355 Notation FortyEight := (nring 48).
359 Infix "{*}" := Fmult (at level 40, left associativity).
363 Infix "{**}" := Fscalmult (at level 40, left associativity).
367 Infix "{^}" := Fnth (at level 30, right associativity).
370 (* From algebra/CSemiGroups ***********************************************)
373 cic:/CoRN/algebra/CSemiGroups/csg_crr.con
377 Infix "[+]" := csg_op (at level 50, left associativity).
381 Infix "{+}" := Fplus (at level 50, left associativity).
384 (* From algebra/CSetoidFun ************************************************)
387 Notation Conj := (conjP _).
391 cic:/CoRN/algebra/CSetoidFun/bpfpfun.con
395 Notation BDom := (bpfdom _ _).
399 cic:/CoRN/algebra/CSetoidFun/pfpfun.con
403 Notation Dom := (pfdom _).
407 Notation Part := (pfpfun _).
411 Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
415 Notation FId := (Fid _).
419 Infix "[o]" := Fcomp (at level 65, no associativity).
423 Notation Prj1 := (prj1 _ _ _ _).
427 Notation Prj2 := (prj2 _ _ _ _).
430 (* From algebra/CSetoids **************************************************)
433 cic:/CoRN/algebra/CSetoids/cs_crr.con
437 Infix "[=]" := cs_eq (at level 70, no associativity).
441 Infix "[#]" := cs_ap (at level 70, no associativity).
445 Infix "[~=]" := cs_neq (at level 70, no associativity).
449 cic:/CoRN/algebra/CSetoids/csp_pred.con
453 cic:/CoRN/algebra/CSetoids/csp'_pred.con
457 cic:/CoRN/algebra/CSetoids/csr_rel.con
461 cic:/CoRN/algebra/CSetoids/Ccsr_rel.con
465 cic:/CoRN/algebra/CSetoids/csf_fun.con
469 cic:/CoRN/algebra/CSetoids/csbf_fun.con
473 cic:/CoRN/algebra/CSetoids/un_op_fun.con
477 cic:/CoRN/algebra/CSetoids/bin_op_bin_fun.con
481 cic:/CoRN/algebra/CSetoids/outer_op_bin_fun.con
485 cic:/CoRN/algebra/CSetoids/scs_elem.con
488 (* From algebra/CVectorSpace **********************************************)
491 cic:/CoRN/algebra/CVectorSpace/vs_vs.con
495 Infix "[']" := vs_op (at level 30, no associativity).
498 (* From algebra/Expon *****************************************************)
501 Notation "( x [//] Hx ) [^^] n" := (zexp x Hx n) (at level 0).
504 (* From complex/CComplex **************************************************)
507 Notation CCX := (cpoly_cring CC).
511 Infix "[+I*]" := cc_set_CC (at level 48, no associativity).
514 (* From fta/CC_Props ******************************************************)
517 cic:/CoRN/fta/CC_Props/CC_seq.con
520 (* From fta/FTAreg ********************************************************)
523 cic:/CoRN/fta/FTAreg/z_el.con
527 cic:/CoRN/fta/FTAreg/Kntup.con
530 (* From ftc/FTC ***********************************************************)
533 Notation "[-S-] F" := (Fprim F) (at level 20).
536 (* From ftc/Integral ******************************************************)
539 Notation Integral := (integral _ _ Hab).
542 (* From ftc/MoreIntervals *************************************************)
545 cic:/CoRN/ftc/MoreIntervals/iprop.con
548 (* From ftc/Partitions ****************************************************)
551 cic:/CoRN/ftc/Partitions/Pts.con
554 (* From ftc/RefLemma ******************************************************)
565 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
569 Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)).
573 Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
576 (* From ftc/RefSeparated **************************************************)
579 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
584 (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__sep_points_lemma _ _)).
587 (* From ftc/RefSeparating *************************************************)
598 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
603 (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__part_pts_in_Partition _ _)).
606 (* From ftc/Rolle *********************************************************)
609 Notation cp := (compact_part a b Hab' d Hd).
612 (* From ftc/TaylorLemma ***************************************************)
615 Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a).
619 Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b).
622 (* From ftc/WeakIVT *******************************************************)
625 Infix "**" := prodT (at level 20).
628 (* From metrics/CMetricSpaces *********************************************)
631 cic:/CoRN/metrics/CMetricSpaces/scms_crr.con
634 (* From metrics/CPseudoMSpaces ********************************************)
637 cic:/CoRN/metrics/CPseudoMSpaces/cms_crr.con
641 Infix "[-d]" := cms_d (at level 68, left associativity).
644 (* From model/structures/Nsec *********************************************)
647 Infix "{#N}" := ap_nat (no associativity, at level 90).
650 (* From model/structures/Qsec *********************************************)
653 Infix "{=Q}" := Qeq (no associativity, at level 90).
657 Infix "{#Q}" := Qap (no associativity, at level 90).
661 Infix "{<Q}" := Qlt (no associativity, at level 90).
665 Infix "{+Q}" := Qplus (no associativity, at level 85).
669 Infix "{*Q}" := Qmult (no associativity, at level 80).
673 Notation "{-Q}" := Qopp (at level 1, left associativity).
677 cic:/CoRN/model/structures/Qsec/inject_Z.con
680 (* From model/structures/Zsec *********************************************)
683 Infix "{#Z}" := ap_Z (no associativity, at level 90).
687 cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2)
690 (* From reals/Bridges_LUB *************************************************)
693 Notation "( p , q )" := (pairT p q).
696 (* From reals/CMetricFields ***********************************************)
699 cic:/CoRN/reals/CMetricFields/cmf_crr.con
703 Notation MAbs := (cmf_abs _).
707 cic:/CoRN/reals/CMetricFields/MCS_seq.con
710 (* From reals/CReals ******************************************************)
713 cic:/CoRN/reals/CReals/crl_crr.con
716 (* From reals/CauchySeq ***************************************************)
719 Notation PartIR := (PartFunct IR).
723 Notation ProjIR1 := (prj1 IR _ _ _).
727 Notation ProjIR2 := (prj2 IR _ _ _).
731 Notation ZeroR := (Zero:IR).
735 Notation OneR := (One:IR).
738 (* From reals/Cauchy_CReals ***********************************************)
741 Notation "'R_COrdField''" := (R_COrdField F).
744 (* From reals/Intervals ***************************************************)
747 Notation Compact := (compact _ _).
751 Notation FRestr := (Frestr (compact_wd _ _ _)).
754 (* From reals/Q_dense *****************************************************)
757 cic:/CoRN/reals/Q_dense/pair_crr.con
761 Notation "( A , B )" := (pairT A B).
764 (* From reals/Q_in_CReals *************************************************)
767 cic:/Coq/NArith/BinPos/nat_of_P.con
770 (* From reals/R_morphism **************************************************)
773 cic:/CoRN/reals/R_morphism/map.con
776 (* From tactics/FieldReflection *******************************************)
779 Notation II := (interpF F val unop binop pfun).
782 (* From tactics/GroupReflection *******************************************)
785 Notation II := (interpG G val unop binop pfun).
788 (* From tactics/RingReflection ********************************************)
791 Notation II := (interpR R val unop binop pfun).
794 (* From transc/RealPowers *************************************************)
797 Notation "x [!] y [//] Hy" := (power x y Hy) (at level 20).
801 Notation "F {!} G" := (FPower F G) (at level 20).
804 (* From devel/loeb/per/lst2fun ********************************************)
807 cic:/CoRN/devel/loeb/per/lst2fun/F_crr.con
811 cic:/CoRN/devel/loeb/per/lst2fun/to_nat.con