Praeclarum theorema
Prove with Lean4 and with Isabelle/HOL the Praeclarum theorema of Leibniz: \[ (p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s)) \]
Prove with Lean4 and with Isabelle/HOL the Praeclarum theorema of Leibniz: \[ (p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s)) \]