search

jjdishere / EG

Formalizing Euclidean Geometry in Lean
26 stars 57 forks source link

More instance of PtNe #268

Open jjdishere opened 6 months ago

jjdishere commented 6 months ago

(SEG A B).isND (TRI A B C).isND (QDR A B C D).isND should give instances PtNe A B

jjdishere commented 6 months ago

参考 https://github.com/leanprover-community/mathlib4/blob/8aa9689f0e48c6fcf9b3ad6846b722c13b7fcd53//Mathlib/Tactic/CategoryTheory/Reassoc.lean