proposition: Fact inZpm_is_additive : additive (inZp : 'Z_n -> 'F_p).
proof: Proof. have p_gt1 : 1 < p by apply: prime_gt1. move=> /= x y; apply/val_eqP/eqP => /=. set x' := nat_of_ord _; set y' := nat_of_ord _. rewrite !Zp_cast /= ?pdiv_id //. rewrite modnDm modnDmr modn_dvdm //. rewrite -modnDmr modnB //; last 2 first. - by apply: leq_trans p_gt1. - apply: ltnW. by have := ltn_ord y; rewrite [X in _ < X -> _]Zp_cast. have -> : modn n p = O%N. by have /dvdnP[k ->] := pDn; rewrite modnMl. rewrite addn0. case: (modn y' p)%N => //= [|xx]; last by rewrite mul1n. by rewrite mul0n !subn0 addn0 modnDr. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound