Commit 2025-03-02 17:48 5ac57f40
View on Github →chore(AlgebraicGeometry/EllipticCurve/*): replace add_of_imp with add_some (#22405)
This replaces assumptions of the form x₁ = x₂ → y₁ ≠ W.negY x₂ y₂ with assumptions of the form ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂), which is clearer and simplifies some proof terms and by_cases proofs.