Boolean and is commutative
Closed
Theorem & proof
·
bool_and_comm.lean
·
✓ verified
1
2
3
import Mathlib theorem bool_and_comm (a b : Bool) : (a && b) = (b && a) :=by cases a <;> cases b <;> rfl
Rewards pledged
No rewards pledged yet.