proposition: Lemma qlogpD (q1 q2 : qT) : q1 != 0 -> q2 != 0 ->qlogp (q1 * q2) = ((qlogp q1 + qlogp q2) %% #|qT|.-1)%N.
proof: Proof. move=> q1_neq0 q2_neq0. apply: qX_exp_inj; [apply: qlogp_lt => // | rewrite ltn_mod // |]. rewrite -[RHS]mul1r -(expr1n _ ((qlogp q1 + qlogp q2) %/ #|qT|.-1)). rewrite -qX_order_card -exprM mulnC -exprD -divn_eq exprD !qlogp_qX //. by rewrite mulf_eq0 negb_or q1_neq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(div bigop binomial finset finfun ssralg countalg finalg) mathcomp(poly polydiv qpoly perm fingroup falgebra fieldext finfield galois) mathcomp(finalg zmodp matrix vector)