proposition: Lemma leq_order_totient k m : 0 < k -> order_modn k m <= totient k.
proof: Proof. move=> k_gt0. case: (leqP k 1) => [|k_gt1]. rewrite /order_modn. by case: k k_gt0 => [|[|]]; rewrite ?ltnn ?andbF. have [kCm|kNCm] := boolP (coprime k m); last first. by rewrite /order_modn coprime_sym (negPf kNCm). rewrite order_modnE //. rewrite -card_units_Zp // /order_modn. case: insubP => //= u uU uE. by apply/subset_leq_card/subsetP=> i; rewrite inE. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)