proposition: Lemma changes_itv_mods_rec a b : a < b -> forall p q, ~~ root (p * q) a -> ~~ root (p * q) b -> changes_itv_mods a b p q = cross (p * q) a b + changes_itv_mods a b q (next_mod p q).
proof: Proof. move=> lt_ab p q rpqa rpqb. have [->|p0] := eqVneq p 0. by rewrite changes_itv_mods0p mul0r next_mod0p changes_itv_modsp0 cross0. have [->|q0] := eqVneq q 0. by rewrite changes_itv_modsp0 mulr0 cross0 changes_itv_mods0p. rewrite /changes_itv_mods /changes_itv_poly /changes_horner neq0_mods_rec //=. rewrite !PoszD opprD addrACA; congr (_ + _); rewrite neq0_mods_rec //=. move: rpqa rpqb; rewrite -!hornerM !rootE; move: (p * q) => r {p q p0 q0}. by rewrite /cross /variation -![_ < _]sgz_cp0 sgzM; do 2!case: sgzP => _. 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)