theorem Regex.OptimizationInfo.findStart_le_pos {s : String} {pos : s.ValidPos} {opt : OptimizationInfo} : pos ≤ opt.findStart pos

theorem Regex.OptimizationInfo.findStart_completeness {s : String} {pos pos' pos'' : s.ValidPos} {opt : OptimizationInfo} {groups : Data.CaptureGroups s} {e : Data.Expr} (eq : opt = fromExpr e) (ge : pos ≤ pos') (lt : pos' < opt.findStart pos) (c : Data.Expr.Captures pos' pos'' groups e) : False