proposition: Lemma introspective1r (R : ringType) n k : n ⋈[k] (1 : {poly R}).
proof: Proof. by rewrite /introspective expr1n comp_polyC polyC1. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound