Theorem: Nat.and_eq_one (Logic/Vorspiel/Arith.lean)

State before:
n m : ℕ
⊢ n.and m = 1 ↔ 0 < n ∧ 0 < m
Tactic:
simp[and_eq, imp_false, Nat.pos_iff_ne_zero]
State after:
no goals