Ceva theorem, first try

Stream: new members

[Anders Larsson]

I have tried to adapt the Ceva theorem proof from Metamath.

Available at: https://gist.github.com/anders-was-here/d786450daba4c01e40bbc5f81c681feb

Original proof/formalization by Saveliy Skresanov: http://us.metamath.org/mpeuni/cevath.html

[Arthur Paulino]

I really like the font you used in some comments btw. I think this is the first time I see it

[Anders Larsson]

Arthur Paulino said:

I really like the font you used in some comments btw. I think this is the first time I see it

It must be unicode. (I think Gists are pure text files). It's cut'n'paste from the Metamath page.

[Yaël Dillies]

Congrats! Have a look at #10632 and a chat with @Mantas Baksys