proposition: Lemma cindex_inv a b : a < b -> forall p q, ~~ root (p * q) a -> ~~ root (p * q) b -> cindex a b q p + cindex a b p q = cross (p * q) a b.
proof: Proof. move=> hab p q hpqa hpqb. have hlab: a <= b by apply: ltW. wlog cpq: p q hpqa hpqb / coprimep p q => [hwlog|]. have p0: p != 0 by apply: contraNneq hpqa => ->; rewrite mul0r rootC. have q0: q != 0 by apply: contraNneq hpqa => ->; rewrite mulr0 rootC. set p' := p; rewrite -(divpK (dvdp_gcdr p q)) -[p'](divpK (dvdp_gcdl p q)). rewrite !cindex_mul2r ?gcdp_eq0 ?(negPf p0) //. have ga0 : (gcdp p q).[a] != 0. apply: contra hpqa; rewrite -rootE -!dvdp_XsubCl => /dvdp_trans -> //. by rewrite dvdp_mulr ?dvdp_gcdl. have gb0 : (gcdp p q).[b] != 0. apply: contra hpqb; rewrite -rootE -!dvdp_XsubCl => /dvdp_trans -> //. by rewrite dvdp_mulr ?dvdp_gcdl. rewrite mulrACA -expr2 cross_pmul ?horner_exp ?exprn_even_gt0 ?ga0 ?gb0 //. apply: hwlog; rewrite ?coprimep_div_gcd ?p0 // rootM. + apply: contra hpqa; rewrite -!dvdp_XsubCl => /orP. case=> /dvdp_trans-> //; rewrite (dvdp_trans (divp_dvd _)); by rewrite ?(dvdp_gcdl, dvdp_gcdr) ?(dvdp_mulIl, dvdp_mulIr). + apply: contra hpqb; rewrite -!dvdp_XsubCl => /orP. case=> /dvdp_trans-> //; rewrite (dvdp_trans (divp_dvd _)); by rewrite ?(dvdp_gcdl, dvdp_gcdr) ?(dvdp_mulIl, dvdp_mulIr). have p0: p != 0 by apply: contraNneq hpqa => ->; rewrite mul0r rootC. have q0: q != 0 by apply: contraNneq hpqa => ->; rewrite mulr0 rootC. have pq0 : p * q != 0 by rewrite mulf_neq0. rewrite cindex_seq_mids // sum_varP /cross. apply: congr_variation; apply: (mulrIz (oner_neq0 R)); rewrite -!sgrEz. case hr: roots => [|c s] /=; apply: (@sgr_neighprN _ _ a b) => //; rewrite /neighpr /next_root ?(negPf pq0) max_l // hr mid_in_itv //=. by move/eqP: hr; rewrite roots_cons => /and5P [_ /itvP ->]. rewrite -cats1 pairmap_cat /= cats1 map_rcons last_rcons. apply: (@sgr_neighplN _ _ a b) => //. rewrite /neighpl /prev_root (negPf pq0) min_l //. by rewrite mid_in_itv //= last_roots_le. elim: roots {-2 6}a (erefl (roots (p * q) a b)) {hpqa hpqb} hab hlab => {a} [|c s IHs] a Hs hab hlab /=. rewrite in_cons orbF eq_sym. by rewrite -rootE (@roots_nil _ _ a b) // mid_in_itv. move/eqP: Hs; rewrite roots_cons => /and5P [_ cab /eqP rac rc /eqP rcb]. rewrite in_cons eq_sym -rootE negb_or (roots_nil _ rac) //=; last first. by rewrite mid_in_itv //= (itvP cab). by rewrite IHs // (itvP cab). 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)