proposition: Lemma cindexR_rec p q : cindexR q p = crossR (p * q) + cindexR (next_mod p q) q.
proof: Proof. have [->|p_neq0] := eqVneq p 0. by rewrite cindexRpC mul0r next_mod0p cindexR0p crossR0. have [->|q_neq0] := eqVneq q 0. by rewrite cindexR0p mulr0 crossR0 cindexRpC. have pq_neq0 : p * q != 0 by rewrite mulf_neq0. pose b := cauchy_bound (p * q). have [lecb gecb] := pair (le_cauchy_bound pq_neq0) (ge_cauchy_bound pq_neq0). rewrite -?(@cindexRP _ _ (-b) b); do ? by [move=> x Hx /=; have: ~~ root (p * q) x by [apply: lecb|apply: gecb]; rewrite rootM => /norP []]. rewrite -(@crossRP _ (-b) b) 1?cindex_rec ?gt0_cp ?cauchy_bound_gt0 //. by rewrite lecb // boundr_in_itv. by rewrite gecb // boundl_in_itv. 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)