proposition: Lemma sqrt3_square : sqrt3* sqrt3 =F= 1+2.
proof: Proof. unfold sqrt3. rewrite PythFOk. rewrite PythFOk. nsatz. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems