proposition: Fact notdiv_pow2_spec_1 n m : notdiv_pow2 n m <> 0 <-> divides (power n 2) m.
proof: Proof. unfold notdiv_pow2. generalize (power n 2); clear n; intros n. unfold ite_rel; case_eq (rem m n). * intros H; split; try discriminate; intros _. exists (div m n). generalize (div_rem_spec1 m n); lia. * intros k Hk; split; try lia; intros H _. apply divides_rem_eq in H; lia. Qed.
imports: Arith List Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list gcd crt sums finite pos vec) Undecidability.MuRec.Util(recalg recomp prim_min)