Add second set of z3py notes

notes/z3py-intro-cont/z3py-intro-cont.md

 It is possible to create such a constraint by asserting inequality for every pair of cells.
 However, since this is such a common pattern, z3 actually provides a function to assert that each variable must take on a *distinct* value. Let's look at this in the context of a [cryptarithm](https://en.wikipedia.org/wiki/Verbal_arithmetic):
 
-<!-- TODO: Magic Square instead? -->
-
 ```python
 # Solve the cryptarithm
 # SEND + MORE = MONEY
 Note that `expr` must evaluate to a `Boolean`.
 
 WARNING: If `cond` evaluates to `False`, `expr` may take on any truth value, i.e. from a false proposition, anything can follow.
-This behavior is different from `cond == expr`.
+This behavior is different from `cond == expr`, which you can think of as "iff".
 
 ### Conditionals Example
 
-TODO
+```python
+p = Bool('p')
+q = Bool('q')
+r = Bool('r')
+x = Int('x')
+# solve is a shortcut to creating a solver, checking, and getting the model
+solve(
+    Implies(p, Not(q)),
+    r == Not(q),
+    Or(Not(p), r),
+    If(p, x == 1, x == 2),
+)
+# [q = True, p = False, x = 2, r = False]
+```
 
 ## Pseudo-Boolean Constraints
 
 The second argument is the bound $`k`$.
 Expressed in Python typing, `PbEq(args: List[Tuple[BoolRef, int]], k: int)`
 
-Example problem and code to solve: $`2q + 2r \leq 2, 2u + 3r \geq 4$.
+Example problem and code to solve: $`2q + 2r \leq 2, 2u + 3r \geq 4`$.
 
 ```python
-solver = Solver()
 q = Bool('q')
 u = Bool('u')
 r = Bool('r')
-solver.add(
-        PbLe([(q, 2), (r, 2)], 3),
-        PbGe([(u, 2), (r, 3)], 4),
-    )
-solver.check()
-print(solver.model())
+solve(
+    PbLe([(q, 2), (r, 2)], 3),
+    PbGe([(u, 2), (r, 3)], 4),
+)
 # [q = False, u = True, r = True]
 ```