proposition: Lemma noroot_cross p a b : a <= b -> {in `]a, b[, noroot p} -> cross p a b = 0.
proof: Proof. move=> le_ab noroot_ab; rewrite /cross /variation. have [] := ltrP; last by rewrite mulr0. rewrite mulr1 -sgr_cp0 sgrM => /eqP. by move=> /(ivt_sign le_ab) [x /noroot_ab /negPf->]. 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)