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

State before:
n m : ℕ
⊢ n.and m = if 0 < n ∧ 0 < m then 1 else 0
Tactic:
simp[and, isLtNat]
State after:
no goals