# Library RulerCompassGeometry.B2_Orient_Prop

Require Export B1_Confondu_Prop.

Section CLOCKWISE_PROPERTIES.

Lemma ClockwiseBCA : forall A B C,
Clockwise A B C -> Clockwise B C A.
Proof.
exact ClockwisePerm.
Qed.

Lemma ClockwiseCAB : forall A B C,
Clockwise A B C -> Clockwise C A B.
Proof.
intros A B C H; do 2 apply ClockwisePerm; trivial.
Qed.

Lemma NotClockwiseAAB : forall A B, ~Clockwise A A B.
Proof.
intros A B; destruct (ClockwiseAntisym A A B); trivial.
Qed.

Lemma NotClockwiseABA : forall A B , ~Clockwise A B A.
Proof.
intros A B H; elim (NotClockwiseAAB A B); apply ClockwiseCAB; trivial.
Qed.

Lemma NotClockwiseBAA : forall A B , ~Clockwise B A A.
Proof.
intros A B H; elim (NotClockwiseAAB A B); apply ClockwiseBCA; trivial.
Qed.

Lemma ClockwiseDistinctAB : forall A B C,
Clockwise A B C -> A <> B.
Proof.
intros A B C H Hi; subst.
elim (NotClockwiseAAB B C); trivial.
Qed.

Lemma ClockwiseDistinctBC : forall A B C,
Clockwise A B C -> B <> C.
Proof.
intros A B C H Hi; subst.
elim (NotClockwiseBAA C A); trivial.
Qed.

Lemma ClockwiseDistinctCA : forall A B C,
Clockwise A B C -> C <> A.
Proof.
intros A B C H Hi; subst.
elim (NotClockwiseABA A B); trivial.
Qed.

Lemma ClockwiseNotClockwise : forall A B C,
Clockwise A B C -> ~Clockwise B A C.
Proof.
intros A B C H H0.
destruct (ClockwiseAntisym A B C); intuition.
Qed.

Lemma ClockwiseClockwiseDistinct : forall A B C D,
Clockwise A B C ->
Clockwise B A D ->
C <> D.
Proof.
intros A B C D H H0 H1; subst.
elim (ClockwiseNotClockwise A B D H); trivial.
Qed.

Lemma ExclusiveFourCases : forall A B C,
A <> C ->
Clockwise A B C \/
Clockwise B A C \/
HalfLine A B C \/
EquiOriented A B C A.
Proof.
intros A B C H; decompose [or] (FourCases A B C).
auto.
auto.
auto.
decompose [or] (FourCases A C B).
generalize (ClockwiseCAB A C B H1); auto.
generalize (ClockwiseBCA C A B); auto.
generalizeChange.
generalizeChange.
Qed.

End CLOCKWISE_PROPERTIES.