proposition: Fact divides_not_0_interval p q : q <> 0 -> divides p q -> 1 <= p <= q.
proof: Proof. intros Hq ([ | k ] & Hk); try lia. Qed.
imports: Arith Lia ZArith List Permutation Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime binomial sums php) Undecidability.H10.ArithLibs(matrix)