The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Hi, since we are talking about geometry and formal proofs,
I hope to not go too much off-topic, but I'm curious about a detail:
---
I know that the oldest proof we know of is:
 We have a square A, we want two square C, D such that the
area(C)+area(D)=area(A) and area(C)=area(D).
if side(A)=1, how much is side(C)?

The answer is sqrt(2)/2 and the proof is:
-cut A using its diagonal.
-recompose the 4 equal pieces into C and D so that sides that was on
the perimeter of A are now the left-right diagonal of
C and D.
-C and D have side equal to half the diagonal of A.
--
  What is obscure for me is in which set of (widely accepted)  axioms
this is true? in which is false? in which is not expressible?
Thanks
Marco.