proposition: Fact ra_minus_val n m : ⟦ra_minus⟧ (n##m##vec_nil) (n-m).
proof: Proof. exists (m##n##vec_nil); split; auto. + rewrite ra_minus_inv_rel; simpl; 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)