proposition: Lemma is_iexp_inj (F : finFieldType) (h : {poly F}) k s (M : {set 'Z_k}) (Q : {set {poly %/ h}}) p q : Mk_spec F s M -> Qh_spec k s Q -> 1 < k -> monic_irreducible_poly h -> rdvdp h ('X^k - 1) -> 1 < p -> is_iexp F k s p -> (1 < q) -> is_iexp F k s q -> (p * q) ^ sqrtn #|M| < #|Q| -> {in Nbar p q (sqrtn #|M|) &, injective (fun i : 'I_ _ => inZp i : 'Z_k)}.
proof: Proof. move=> hMK hQh k_gt1 hMI hDxk1 p_gt1 pIN q_gt1 qIN pqLqh i j iIN jIN. move=> /(congr1 val); rewrite /= [X in _ = _ %[mod X]]Zp_cast // => imEjm. have k_gt0 : 0 < k by rewrite -ltnS ltnW. pose r := map_poly (qfpoly_const hMI) ('X^i - 'X^j). suff : r == 0. rewrite /r rmorphB /= subr_eq0 => /eqP/map_poly_div_inj. move=> /(congr1 (size : {poly F} -> nat)). by rewrite !size_polyXn => [] [] /eqP /val_eqP. apply/eqP/(@roots_geq_poly_eq0 (GRing.IntegralDomain.clone _ {poly %/ h with hMI}) _ (enum Q)). - apply/allP => /= x. rewrite mem_enum; case: hQh => // p1 -> p1I _. apply/eqP; rewrite -in_qpoly_comp_horner. apply: is_iexp_root p1I => //. case/imsetP: jIN => [[i1 j1] _ -> /=]. rewrite modn_small. by apply: is_iexp_mul; apply: is_iexp_X. by rewrite ltnS expnMn leq_mul // leq_exp2l // -ltnS. case/imsetP: iIN => [[i1 j1] _ -> /=]. rewrite modn_small. by apply: is_iexp_mul; apply: is_iexp_X. by rewrite ltnS expnMn leq_mul // leq_exp2l // -ltnS. - by apply: enum_uniq. rewrite -cardE. apply: leq_trans pqLqh. rewrite /r rmorphB /= !map_polyXn. apply: leq_trans (size_add _ _) _. by rewrite size_opp !size_polyXn geq_max !ltn_ord. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound