proposition: Fact ra_mult_val n m : ⟦ra_mult⟧ (n##m##vec_nil) (n*m).
proof: Proof. simpl; unfold s_rec; simpl. induction n as [ | n IHn ]; simpl in *. + cbv; trivial. + exists (n*m); split; auto. exists ((n*m)##m##vec_nil); split. * apply ra_plus_rel; simpl; ring. * intros p; analyse pos p; cbv; trivial. 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)