proposition: Lemma introspecMr (R : comRingType) (k n : nat) (p q : {poly R}) : n ⋈[k] p -> n ⋈[k] q -> n ⋈[k] (p * q).
proof: Proof. case: k => [|k nIp nIq]. rewrite /introspective !subrr !rmodp0. by rewrite comp_polyM exprMn => /eqP-> /eqP->. have Xlf := monic_Xn_sub_1 R (isT : 0 < k.+1). rewrite /introspective exprMn -rmodp_mulmr // (eqP nIq). rewrite rmodp_mulmr // mulrC. rewrite -rmodp_mulmr // (eqP nIp) rmodp_mulmr //. by rewrite mulrC comp_polyM. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound