proposition: Fact ra_inject_val n v : ⟦ra_inject n⟧ v (inject v).
proof: Proof. induction n as [ | n IHn ]; simpl. + vec nil v; simpl; auto. + vec split v with x. exists (x##inject v##vec_nil); split. * apply ra_recomp_val. * pos split; simpl; auto. exists v; split; auto. intro; vec pos simpl. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_nat gcd crt sums) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.MuRec.Util(recalg recomp prim_min ra_utils)