There are two lemmas about integration at the end of trigo.v. They are requiring ftc.v, and hence all its dependencies (almost all of Lebesgue stieltjes integration theory).
I felt it very inconvenient when I just wanted to use the definition and some basic properties of cos/sin.
What about separating integration lemmas for trigo into some file like trigo_integral. v?
https://rocq-prover.zulipchat.com/#narrow/channel/268055-math-comp-analysis-private/topic/integration.20lemmas.20in.20trigo.2Ev.20inducing.20huge.20dependencies/with/612704297
There are two lemmas about integration at the end of trigo.v. They are requiring ftc.v, and hence all its dependencies (almost all of Lebesgue stieltjes integration theory).
I felt it very inconvenient when I just wanted to use the definition and some basic properties of cos/sin.
What about separating integration lemmas for trigo into some file like trigo_integral. v?
https://rocq-prover.zulipchat.com/#narrow/channel/268055-math-comp-analysis-private/topic/integration.20lemmas.20in.20trigo.2Ev.20inducing.20huge.20dependencies/with/612704297