Theorem: L3 (LeanTeaching/Ex2/1.lean)

State before:
P Q R : Prop
h : P ∨ R ∨ Q → ¬(R ∧ Q ∧ P)
⊢ R ∨ Q ∨ P → ¬((P ∧ Q) ∧ R)
Tactic:
sorry
State after:
no goals