proposition: Fact ra_choice3_spec b x y z d : (b = 0 -> d = x) -> (b = 1 -> d = y) -> (2 <= b -> d = z) -> ⟦ra_choice3⟧ (b##x##y##z##vec_nil) d.
proof: Proof. intros H1 H2 H3. destruct b as [ | [] ]. + rewrite H1; auto; apply ra_choice3_val. + rewrite H2; auto; apply ra_choice3_val. + rewrite H3; try lia. apply ra_choice3_val. 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)