proposition: Lemma card_units_Zp : p > 0 -> #|units_Zp| = totient p.
proof: Proof. move=> p_gt0; transitivity (totient p.-2.+2); last by case: p p_gt0 => [|[|p']]. rewrite cardsT card_sub -sum1_card big_mkcond /=. by rewrite totient_count_coprime big_mkord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)