ftc/Make at master · verimath/ftc · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
-R src/ftc FTC -R src/reals Reals -R src/algebra Algebra -R src/tactics Tactics

src/tactics/CTactics.v
src/tactics/rational.ml
src/ftc/CalculusTheorems.v
src/ftc/Composition.v
src/ftc/Continuity.v
src/ftc/Derivative.v
src/ftc/DerivativeOps.v
src/ftc/Differentiability.v
src/ftc/FTC.v
src/ftc/FunctSequence.v
src/ftc/FunctSeries.v
src/ftc/FunctSums.v
src/ftc/FunctTactics.v
src/ftc/Integral.v
src/ftc/IntegralLemmas.v
src/ftc/IntervalFunct.v
src/ftc/MoreFunSeries.v
src/ftc/MoreFunTactics.v
src/ftc/MoreFunctions.v
src/ftc/MoreIntegrals.v
src/ftc/MoreIntervals.v
src/ftc/NthDerivative.v
src/ftc/PartFunEquality.v
src/ftc/PartInterval.v
src/ftc/Partitions.v
src/ftc/RefLemma.v
src/ftc/RefSepRef.v
src/ftc/RefSeparated.v
src/ftc/RefSeparating.v
src/ftc/Rolle.v
src/ftc/StrongIVT.v
src/ftc/Taylor.v
src/ftc/TaylorLemma.v
src/ftc/WeakIVT.v
src/reals/CMetricFields.v
src/reals/CPoly_ApZero.v
src/reals/CPoly_Contin.v
src/reals/CReals.v
src/reals/CReals1.v
src/reals/CSumsReals.v
src/reals/CauchySeq.v
src/reals/IVT.v
src/reals/Intervals.v
src/reals/Max_AbsIR.v
src/reals/NRootIR.v
src/reals/OddPolyRootIR.v
src/reals/RealFuncts.v
src/reals/RealLists.v
src/reals/Series.v
src/algebra/Basics.v
src/algebra/CFields.v
src/algebra/CGroups.v
src/algebra/CLogic.v
src/algebra/CMonoids.v
src/algebra/COrdFields.v
src/algebra/CPoly_Degree.v
src/algebra/CPoly_NthCoeff.v
src/algebra/CPolynomials.v
src/algebra/CRings.v
src/algebra/CSemiGroups.v
src/algebra/CSetoids.v
src/algebra/CSums.v
src/algebra/CVectorSpace.v
src/algebra/Expon.v
src/algebra/Opaque_algebra.v
src/algebra/PFunct.v
src/algebra/RRefl_corr.v
src/algebra/RReflection.v
src/algebra/Refl_corr.v
src/algebra/Reflection.v
src/algebra/Transparent_algebra.v