# Library RulerCompassGeometry.C6_Parallele_Prop

Require Export C5_Droite_Prop.

Section EQUIDIRECTED_PROPERTIES.

Lemma EquiDirectedRefl : forall A B : Point,
EquiDirected A B A B.
Proof.
canonize.
Qed.

Lemma EquiDirectedSym : forall A B C D : Point,
EquiDirected A B C D ->
EquiDirected C D A B.
Proof.
canonize.
Qed.

Lemma EquiDirectedPermut : forall A B C D : Point,
EquiDirected A B C D ->
EquiDirected B A C D.
Proof.
canonize.
Qed.

Lemma EquiDirectedPermutCD: forall A B C D : Point,
EquiDirected A B C D ->
EquiDirected A B D C.
Proof.
intros; apply EquiDirectedSym; apply EquiDirectedPermut;
apply EquiDirectedSym; trivial.
Qed.

Lemma ParallelNotClockwiseABC : forall A B C D,
EquiOriented A B C D ->
~Clockwise A B C.
Proof.
canonize.
elim (NotClockwiseABA C D); auto.
Qed.

Lemma ParallelNotClockwiseABD : forall A B C D,
EquiOriented A B C D ->
~Clockwise A B D.
Proof.
canonize.
elim (NotClockwiseBAA D C); auto.
Qed.

Lemma ParallelCollinearABD : forall A B C D,
EquiOriented A B C D ->
Collinear A B C ->
Collinear A B D.
Proof.
canonize.
elim (NotClockwiseBAA D C); auto.
destruct (CollinearHalfLine A B C).
canonize.
generalizeChange.
elim (NotClockwiseBAA A B); apply H3.
autoDistinct.
assert (Clockwise C A D); [ auto | autoClockwise ].
generalizeChange.
elim (HalfLineNotClockwiseBAC C B D).
canonize.
apply H; apply H5.
autoDistinct.
trivial.
canonize.
Qed.

Lemma ParallelCollinearABC : forall A B C D,
EquiOriented A B C D ->
Collinear A B D ->
Collinear A B C.
Proof.
canonize.
elim (NotClockwiseABA C D); auto.
destruct (CollinearHalfLine A B D).
canonize.
generalizeChange.
elim (HalfLineNotClockwiseBAC D C A).
canonize.
apply H6; apply H3.
autoDistinct.
trivial.
assert (Clockwise D A C).
auto.
autoClockwise.
generalizeChangeSide.
elim (NotClockwiseABA B A); apply H3.
autoDistinct.
assert (Clockwise B D C).
auto.
autoClockwise.
Qed.

Lemma ParallelCollinearCDB : forall A B C D,
EquiOriented A B C D ->
Collinear C D A ->
Collinear C D B.
Proof.
canonize.
destruct (CollinearHalfLine C D A).
canonize.
elim (NotClockwiseABA C D); apply H.
generalize (H3 B H0); intro; autoClockwise.
elim (HalfLineNotClockwiseBAC A B D).
generalizeChange.
assert (Clockwise A D B).
generalizeChange.
autoClockwise.
elim (NotClockwiseABA B A).
generalizeChange.
apply H3.
apply (CollinearClockwiseDistinct D C A B).
canonize.
auto.
auto.
Qed.

Lemma ParallelCollinearCDA : forall A B C D,
EquiOriented A B C D ->
Collinear C D B ->
Collinear C D A.
Proof.
canonize.
destruct (CollinearHalfLine C D B).
canonize.
elim (HalfLineNotClockwiseBAC B C A).
generalizeChange.
apply H3.
intro; destruct (CollinearClockwiseDistinct C D B A); canonize.
apply H6.
autoDistinct.
trivial.
generalizeChange.
elim (NotClockwiseBAA D C); apply H.
assert (Clockwise B D A).
generalizeChange.
autoClockwise.
generalizeChangeSide.
elim (NotClockwiseBAA A B); apply H3.
intro; destruct (CollinearClockwiseDistinct D C B A); canonize.
trivial.
Qed.

End EQUIDIRECTED_PROPERTIES.