search

jjdishere / EG

Formalizing Euclidean Geometry in Lean
26 stars 57 forks source link

Congruence exercise ygr 1-4 #272

Closed Thmoas-Guan closed 5 months ago

Thmoas-Guan commented 6 months ago

1,2,4 is complete 3 still need qdr_cvx to be complete add translation between cclock and odist add relative side (at Orientation)