proposition: Lemma poly_order_rmod_inj (R : ringType) (h : {poly R}) k m n : h \is monic -> 1 < size h -> 0 < k -> rdvdp h ('X^k - 1) -> m < poly_order h 'X k -> n < poly_order h 'X k -> rmodp 'X^m h = rmodp 'X^n h-> m = n.
proof: Proof. move=> hM hS k_gt0 hDxk. wlog : m n / m <= n => [Hw |mLn] mLp nLp xmExn. case: (leqP m n) => [/Hw|nLm]; first by apply. by apply/sym_equal/Hw => //; apply: ltnW. move: mLn; rewrite leq_eqVlt => /orP[/eqP//|mLn]. have xkE1 : rmodp 'X^k h = 1. move: hDxk; rewrite /rdvdp rmodpB // [rmodp 1 _]rmodp_small. by rewrite subr_eq0 => /eqP. by rewrite size_polyC oner_neq0. have [|o_gt0] := leqP (poly_order h 'X k) 0. have kB : 0 < k <= k by rewrite k_gt0 leqnn. by rewrite leqn0 => /eqP/poly_order_eq0_rmodp /(_ kB) /eqP[]. pose v := (poly_order h 'X k - n + m)%N. have /poly_order_lt/eqP[] : (0 < poly_order h 'X k - n + m < poly_order h 'X k )%nat. rewrite (leq_trans _ (_ : 0 + m < _)) //; last first. by rewrite ltn_add2r subn_gt0. rewrite -{2}[poly_order _ _ _](@subnK m); last by apply: ltnW. by rewrite ltn_add2r ltn_sub2l //. rewrite exprD -rmodp_mulmr // xmExn rmodp_mulmr // -exprD subnK //. by apply/eqP/poly_order_gt0_rmodp. by apply/ltnW. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound