proposition: Fact divides_n_fact_n n : 0 < n -> divides n (fact n).
proof: Proof. destruct n as [ | n ]; try lia; intros _. apply divides_mult_r, divides_refl. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd)