proposition: Lemma vec_sum_le: forall (k : nat) (cst : vec nat k) (j : pos k), vec_pos cst j <= vec_sum cst.
proof: Proof. intros k cst j. induction cst; cbn. - invert pos j. - invert pos j. + lia. + specialize (IHcst j); lia. Qed.
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.L.Datatypes(LNat LOptions LSum) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared(DLW.Utils.finite DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec(MuRec recalg ra_sem_eq)