Disjunction is symmetric
Closed
Theorem & proof
·
or_symm.lean
·
✓ verified
1
2
3
import Mathlib theorem or_symm {p q : Prop} (h : p ∨ q) : q ∨ p :=Or.symm h
Rewards pledged
No rewards pledged yet.