Complete proof coverage: Bool binary, Prop connectives, Relational LE

**Goal:** Close the residual emission gaps in the Bool `&&`/`||`/`!` and Prop `∧`/`∨`/`¬` reductions, add LE coverage, and flag every reconstructing Bool/Prop test.

**Scope:**
```
Simple emission gaps (direct proof step):
True ∧ True ==> True, False ∨ True / True ∨ False ==> True
¬ (Nat.ble / Nat.blt c1 c2) ==> True / False
!(a == b) ==> ¬ (a = b) (confirm it is not a BEq case)
Let-chain composition cases (may be a replay issue, not new rules):
e && not e, e || not e, true && e, ¬ (true/false = e), reached through lets
Relational:
a ≤ b ==> ¬ (b < a) (Nat, Int; tests only, already emits)
x ≥ y ==> y ≤ x (Nat, Int; new emission, where GE.ge is unfolded in Basic.lean)
```

**Out of scope:** the ITE-splitting cases `BoolNotUnchanged_5` / `NotUnchanged_5` (ITE normalization, out of Milestone 1), DecideEq, BEq.

**DoD:**
- [x] Each simple in-scope gap pushes its proof step.
- [x] The let-chain composition cases reconstruct, or are logged as a replay issue if they emit piecewise but fail on replay.
- [x] A `#testOptimize [ ..., proof ]` test exercises each in-scope case, including LE and GE (Nat, Int), wired into `Tests/Optimize.lean`.
- [ ] Every reconstructing test in the Bool and Prop suites carries the `proof` flag.