proposition: Fact divides_trans x y z : x div y -> y div z -> x div z.
proof: Proof. intros (p & H1) (q & H2). exists (q*p); rewrite <- Nat.mul_assoc, <- H1; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)