proposition: Fact divides_fact_lt q n : 1 <= q <= n -> divides q (fact n).
proof: Proof. revert q; induction n as [ | n IHn ]. + intros; rewrite fact_0; lia. + intros q Hq; rewrite fact_S. destruct (eq_nat_dec q (S n)). - subst; exists (fact n); ring. - apply divides_mult, IHn; 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)