proposition: Lemma power_factor_lt_neq p i j x y : p <> 0 -> i < j -> ~ divides p x -> p^i * x <> p^j * y.
proof: Proof. intros H1 H2 H3 H5. replace j with (i+S (j-i-1)) in H5 by lia. rewrite Nat.pow_add_r, <- Nat.mul_assoc in H5. rewrite Nat.mul_cancel_l in H5. 2: apply Nat.pow_nonzero; auto. apply H3; subst x; simpl. do 2 apply divides_mult_r; apply divides_refl. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)