proposition: Lemma ra_ca_min_inv k f v n x : [@ra_min k f;v] -[n>> x -> exists p w q, n = 1+p+vec_sum q /\ [f;x##v] -[p>> 0 /\ forall j, [f;pos2nat j##v] -[vec_pos q j>> S (@vec_pos _ x w j).
proof: Proof. myauto; ra_inj. exists q', w', m'; auto. Qed.
imports: Arith Eqdep_dec Undecidability.Shared(DLW.Utils.utils DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec.Util(recalg)