proposition: Lemma power_factor_uniq p i j x y : p <> 0 -> ~ divides p x -> ~ divides p y -> p^i * x = p^j * y -> i = j /\ x = y.
proof: Proof. intros H1 H2 H3 H4. destruct (lt_eq_lt_dec i j) as [ [ H | H ] | H ]. + exfalso; revert H4; apply power_factor_lt_neq; auto. + split; auto; subst j. rewrite Nat.mul_cancel_l in H4; auto. apply Nat.pow_nonzero; auto. + exfalso; symmetry in H4; revert H4; apply power_factor_lt_neq; auto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)