proposition: Lemma divides_mult_inv_l p q r : p * q div r -> p div r /\ q div r.
proof: Proof. intros []; split; subst. - exists (x * q); ring. - exists (x * p); ring. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)