proposition: Fact modS_divide n p : p mod S n = 0 <-> S n <d p.
proof: Proof. unfold divides. split. - intros E. rewrite (Nat.div_mod_eq p (S n)). exists (p / S n). lia. - intros [k ->]. generalize (Nat.div_mod_eq (k * (S n)) (S n)). rewrite Nat.div_mul; lia. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)