docs: clarify condition ordering and improve wording

Author: mkovaxx

README.md

@@ -85,9 +85,9 @@ Contracts are built from conditions, which come in three flavors:
 
 - **Invariants** (using `maintains: <conditions>`): A convenience for conditions that must hold true both before and after the function runs. It's most useful for expressing properties of `self` that a method must preserve.
 
-For convenience `<conditions>` can be either a single condition or a list (i.e. `[<condition>, <condition>, ...]`).
+For convenience, `<conditions>` can be either a single condition or a list (i.e. `[<condition>, <condition>, ...]`).
 
-The conditions must be given in the following order: `requires`, `maintains`, and `ensures`.
+The conditions must be given in the following order: `requires`, `maintains`, and `ensures`. This order is enforced to mirror the logical flow of a function's execution: preconditions (`requires`) are checked upon entry, invariants (`maintains`) must hold true upon both entry and exit, and postconditions (`ensures`) are checked upon exit.
 
 A condition is a `bool`-valued Rust expression; as simple as that. This is a non-trivial design choice, so its benefits are explained in the section below: [Why Conditions Are Rust Expressions](#why-conditions-are-rust-expressions).