proposition: Fact ra_pow2_val n : ⟦ra_pow2⟧ (n##vec_nil) (power n 2).
proof: Proof. exists (n##2##vec_nil); split. + apply ra_exp_val; discriminate. + 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)