proposition: Lemma inv_exp q p1 p2 x y : q <> 0 -> ~ divides q p1 -> ~ divides q p2 -> q ^ x * p1 = q ^ y * p2 -> x = y.
proof: Proof. intros H1 H2 H3 H4. apply power_factor_uniq in H4; tauto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)