proposition: Lemma changes_mods_rec p q : changes_mods p q = crossR (p * q) + changes_mods q (next_mod p q).
proof: Proof. have [->|p0] := eqVneq p 0. by rewrite changes_mods0p mul0r crossR0 next_mod0p changes_modsp0. have [->|q0] := eqVneq q 0. by rewrite changes_modsp0 mulr0 crossR0 changes_mods0p. rewrite /changes_mods /changes_poly neq0_mods_rec //=. rewrite !PoszD opprD addrACA; congr (_ + _); rewrite neq0_mods_rec //=. rewrite /crossR /variation /sgp_pinfty /sgp_minfty. rewrite mulr_signM size_mul // !lead_coefM. rewrite polySpred // addSn [size q]polySpred // addnS /= !negbK. rewrite -oddD signr_odd; set s := _ ^+ _. rewrite -!sgz_cp0 !(sgz_sgr, sgzM). have: s != 0 by rewrite signr_eq0. by move: p0 q0; rewrite -!lead_coef_eq0; do 3!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)