proposition: Fact divides_fact n i : 0 < i <= n -> divides i (fact n).
proof: Proof. intros (H1 & H2); revert H2. induction 1 as [ | n H2 IH2 ]. + apply divides_n_fact_n; auto. + apply divides_trans with (1 := IH2), divides_fact_S. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd)