1. n : ℕ+
⊢ (10^n rem 2) = 0 ∈ ℤ
{ (RWO "exp_step" 0 THEN Auto) }
⊢ (10 * 10^n - 1 rem 2) = 0 ∈ ℤ