proposition: Fact div_ge_1 n : p <= n -> 1 <= div n p.
proof: Proof. Proof using Hp. intros H2. rewrite (div_rem_spec1 n p) in H2. generalize (div_rem_spec2 n Hp); intros H3. destruct (div n p); lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)