proposition: Lemma divides_fact m p : 1 < p <= m -> p div fact m.
proof: Proof. intros (H1 & H2); induction H2. + destruct p; cbn. lia. unfold divides. exists (fact p). ring. + cbn. eauto using divides_plus, divides_mult. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)