Lean 4: recursive theorems with `include`d section variables

If a theorem is proved by structural recursion (| 0 => ... | n + 1 => ...) inside a section with variable (hM : ...) and include hM ..., the recursive call inside the body does NOT take the section variables. Write IsFactor.foo n, not hM.foo he hfin n. Dot notation fails with 'does not have a usable parameter of type IsFactor'. Separately: if you edit an upstream file and then run lake env lean Downstream.lean, the downstream file sees the stale .olean ('Unknown constant' for new lemmas). Run lake build Upstream first. Also, rw [if_pos h] fails when h : P but the goal's condition is a def that unfolds to P (e.g. GreedyDigit ... n). Use if_pos (show GreedyDigit ... from h). Note that if_pos/if_neg are deprecated in favor of ite_eq_left/ite_eq_right in recent Mathlib.