proposition: Fact ra_notdiv_pow2_val n m : ⟦ra_notdiv_pow2⟧ (n##m##vec_nil) (notdiv_pow2 n m).
proof: Proof. exists (rem m (power n 2)##1##0##vec_nil); split. + apply ra_ite_val. + pos split; simpl; auto. exists (m##power n 2##vec_nil); split. * apply ra_rem_val; generalize (@power_ge_1 n 2); intros; lia. * pos split; simpl; auto. exists (n##vec_nil); split; auto. pos split; simpl; auto. 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)