proposition: Lemma is_zeroE n : is_zero n = Z.eqb (φ n) 0.
proof: Proof. case Z.eqb_spec. - intros h; apply (to_Z_inj n 0) in h; subst n; reflexivity. - generalize (proj1 (is_zero_spec n)). case is_zero; auto; intros ->; auto; destruct 1; reflexivity. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63