proposition: Lemma crossRP p a b : {in `]-oo, a], noroot p} -> {in `[b , +oo[, noroot p} -> cross p a b = crossR p.
proof: Proof. move=> rpa rpb; rewrite /crossR /cross. rewrite -(@sgp_minftyP _ _ _ rpa a) ?boundr_in_itv //. rewrite -(@sgp_pinftyP _ _ _ rpb b) ?boundl_in_itv //. by rewrite /variation -sgrM sgr_lt0 sgz_sgr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)