proposition: Lemma Zmod_m1_l a : 0 < a -> (-1) mod a = a - 1.
proof: Proof. intros ha. destruct (Z.eq_dec a 1) as [-> | a1]. reflexivity. transitivity ((a - 1) mod a). - rewrite Zminus_mod, Z_mod_same, Zmod_1_l. reflexivity. lia. lia. - apply Z.mod_small. lia. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)