theorem String.Slice.Pattern.Internal.memcmpStr_eq_true_iff {lhs rhs : String} {lstart rstart len : Pos.Raw} {h₁ : len.offsetBy lstart ≤ lhs.rawEndPos} {h₂ : len.offsetBy rstart ≤ rhs.rawEndPos} : memcmpStr lhs rhs lstart rstart len h₁ h₂ = true ↔ lhs.toByteArray.extract lstart.byteIdx (len.offsetBy lstart).byteIdx = rhs.toByteArray.extract rstart.byteIdx (len.offsetBy rstart).byteIdx

theorem String.Slice.Pattern.Internal.memcmpSlice_eq_true_iff {lhs rhs : Slice} {lstart rstart len : Pos.Raw} {h₁ : len.offsetBy lstart ≤ lhs.rawEndPos} {h₂ : len.offsetBy rstart ≤ rhs.rawEndPos} : memcmpSlice lhs rhs lstart rstart len h₁ h₂ = true ↔ lhs.copy.toByteArray.extract lstart.byteIdx (len.offsetBy lstart).byteIdx = rhs.copy.toByteArray.extract rstart.byteIdx (len.offsetBy rstart).byteIdx