Proof Certificates and Geometry

Definitions

Record point:Type := { X:R; Y:R}.

Definition collinear(A B C:point):=
  (X A - X B) * (Y C - Y B) - (Y A - Y B) * (X C - X B) = 0.

Definition parallel (A B C D:point):=
  ((X A) - (X B)) * ((Y C) - (Y D)) = ((Y A) - (Y B)) * ((X C) - (X D)).

Definition notparallel (A B C D:point)(x:R):=
  x* (((X A) - (X B)) * ((Y C) - (Y D)) - ((Y A) - (Y B)) * ((X C) - (X D))) = 1.

Definition orthogonal (A B C D:point):=
  ((X A) - (X B)) * ((X C) - (X D)) + ((Y A) - (Y B)) * ((Y C) - (Y D)) = 0.

Definition equal2(A B:point):=
  (X A) = (X B) /\ (Y A) = (Y B).

Definition equal3(A B:point):=
  ((X A) - (X B))^2 + ((Y A) - (Y B))^2 = 0.

Definition nequal2(A B:point):=
  (X A) <> (X B) \/ (Y A) <> (Y B).

Definition nequal3(A B:point):=
  not (((X A) - (X B))^2 + ((Y A) - (Y B))^2 = 0).

Definition middle(A B I:point):=
  2* (X I) = (X A) + (X B) /\ 2 * (Y I)= (Y A) + (Y B).

Definition distance2(A B:point):=
  ((X B) - (X A))^2 + ((Y B) - (Y A))^2.

Definition equaldistance(A B C D:point):=
  ((X B) - (X A))^2 + ((Y B) - (Y A))^2 = ((X D) - (X C))^2 + ((Y D) - (Y C))^2.

Definition determinant(A O B:point):=
  ((X A) - (X O)) * ((Y B) - (Y O)) - ((Y A) - (Y O)) * ((X B) - (X O)).

Definition scalarproduct(A O B:point):=
  ((X A) - (X O)) * ((X B) - (X O)) + ((Y A) - (Y O)) * ((Y B) - (Y O)).

Definition norm2(A O B:point):=
  (((X A) - (X O))^2 + ((Y A) - (Y O))^2) * (((X B) - (X O))^2 + ((Y B) - (Y O))^2).

Definition tripletangente(A B C D E F:point):=
  let s:= determinant A B C in
  let c:= scalarproduct A B C in
  let s3:= determinant D E F in
  let c3:= scalarproduct D E F in
  s^3 * c3 - 3 * s3 * s^2 * c - 3 * s * c^2 * c3 + s3 * c^3 = 0.

Definition equalangle(A B C D E F:point):=
  let s1:= determinant A B C in
  let c1:= scalarproduct A B C in
  let n1:= norm2 A B C in
  let s2:= determinant D E F in
  let c2:= scalarproduct D E F in
  let n2:= norm2 D E F in
  s1 * n2 = s2 * n1 /\ c1 * n2 = c2 * n1.

Definition equaltangente(A B C D E F:point):=
  let s1:= determinant A B C in
  let c1:= scalarproduct A B C in
  let s2:= determinant D E F in
  let c2:= scalarproduct D E F in
  s1 * c2 = s2 * c1.

Examples