proposition: Lemma cindex_rec a b : a < b -> forall p q, ~~ root (p * q) a -> ~~ root (p * q) b -> cindex a b q p = cross (p * q) a b + cindex a b (next_mod p q) q.
proof: Proof. move=> lt_ab p q rpqa rpqb; have [->|p0] := eqVneq p 0. by rewrite cindexpC next_mod0p cindex0p mul0r cross0 add0r. have [->|q0] := eqVneq q 0. by rewrite cindex0p cindexpC mulr0 cross0 add0r. have /(canRL (addrK _)) -> := cindex_inv lt_ab rpqa rpqb. by rewrite cindex_mulCp cindex_mod sgzN mulNr sgzX. 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)