proposition: Lemma integral_add u v : integralOver RtoK u -> integralOver RtoK v -> integralOver RtoK (u + v).
proof: Proof. by rewrite -{2}[v]opprK => intRu /integral_opp; apply: integral_sub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)