Si (m ∣ n ∧ m ≠ n), entonces (m ∣ n ∧ ¬(n ∣ m))
Demostrar con Lean4 que si (m ∣ n ∧ m ≠ n), entonces (m ∣ n ∧ ¬(n ∣ m)).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Nat.GCD.Basic variable {m n : ℕ} example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := by sorry |