# Library RulerCompassGeometry.B11_Angle_prop

Require Export B10_Longueur_Prop.

Section ANGLE_PROPERTIES.

Lemma AngleSym : forall A B C : Point,
A <> B ->
A <> C ->
Angle B A C = Angle C A B.
Proof.
intros; apply CongruentItself; canonize.
Qed.

Lemma HalfLineAngleB : forall A B C D : Point,
A <> B ->
A <> C ->
HalfLine A B D ->
Angle B A C = Angle D A C.
Proof.
intros; rewrite AngleSym; auto.
apply CongruentItself; canonize.
Qed.

Lemma HalfLineAngleC : forall A B C D : Point,
A <> B ->
A <> C ->
HalfLine A C D ->
Angle B A C = Angle B A D.
Proof.
intros; rewrite AngleSym; auto.
apply CongruentItself; canonize.
Qed.

Lemma HalfLineAngleBC : forall A B C D E : Point,
A <> B ->
A <> C ->
HalfLine A B D ->
HalfLine A C E ->
Angle B A C = Angle D A E.
Proof.
intros; rewrite AngleSym; auto.
apply CongruentItself; canonize.
Qed.

Lemma BetweenAngleBC : forall A B C D E : Point,
Between A B D ->
Between A C E ->
Angle B A C = Angle D A E.
Proof.
intros; apply HalfLineAngleBC.
apply (BetweenDistinctAB _ _ _ H).
apply (BetweenDistinctAB _ _ _ H0).
apply (BetweenHalfLine _ _ _ H).
apply (BetweenHalfLine _ _ _ H0).
Qed.

Lemma BetweenAngleC : forall A B C D : Point,
A <> B ->
Between A C D ->
Angle B A C = Angle B A D.
Proof.
intros; apply HalfLineAngleC.
trivial.
apply (BetweenDistinctAB _ _ _ H0).
apply (BetweenHalfLine _ _ _ H0).
Qed.

Lemma BetweenAngleB : forall A B C D : Point,
A <> C ->
Between A B D ->
Angle B A C = Angle D A C.
Proof.
intros; apply HalfLineAngleB.
apply (BetweenDistinctAB _ _ _ H0).
trivial.
apply (BetweenHalfLine _ _ _ H0).
Qed.

Lemma SASEqualBD : forall A B C D : Point,
Clockwise A B C ->
Clockwise A D C ->
Distance A B = Distance A D ->
Angle B A C = Angle D A C ->
B = D.
Proof.
intros; apply (SSSEqualBD A B C D); auto.
apply (CongruentSAS A B C A D C); auto.
exact (ClockwiseDistinctAB A B C H).
exact (sym_not_eq (ClockwiseDistinctCA A B C H)).
Qed.

Lemma SASEqualCD : forall A B C D : Point,
Clockwise A B C ->
Clockwise A B D ->
Distance A C = Distance A D ->
Angle B A C = Angle B A D ->
C = D.
Proof.
intros; apply (SSSEqualCD A B C D); auto.
apply (CongruentSAS A B C A B D); auto.
exact (ClockwiseDistinctAB A B C H).
exact (sym_not_eq (ClockwiseDistinctCA A B C H)).
Qed.

Lemma AngleBHalfLine : forall A B C D : Point,
Clockwise A B C ->
Clockwise A D C ->
Angle B A C = Angle D A C ->
HalfLine A B D.
Proof.
intros.
assert (Hab := ClockwiseDistinctAB A B C H).
assert (Had := ClockwiseDistinctAB A D C H0).
destruct (ExistsHalfLineEquidistant A B A D Hab Had) as (E, (H2, H3)).
rewrite (SASEqualBD A D C E H0).
trivial.
canonize.
auto.
rewrite <- H1; apply HalfLineAngleB; auto.
exact (sym_not_eq (ClockwiseDistinctCA A B C H)).
Qed.

Lemma AngleCHalfLine : forall A B C D : Point,
Clockwise A B C ->
Clockwise A B D ->
Angle B A C = Angle B A D ->
HalfLine A C D.
Proof.
intros.
assert (Hac := sym_not_eq (ClockwiseDistinctCA A B C H)).
assert (Had := sym_not_eq (ClockwiseDistinctCA A B D H0)).
destruct (ExistsHalfLineEquidistant A C A D Hac Had) as (E, (H2, H3)).
rewrite (SASEqualCD A B D E H0).
trivial.
generalizeChangeSense.
apply ClockwiseBCA; apply H4; apply ClockwiseCAB; trivial.
auto.
rewrite <- (HalfLineAngleC A B C E); auto.
exact (ClockwiseDistinctAB A B C H).
Qed.

End ANGLE_PROPERTIES.

Section PARTICULAR_ANGLES.

Definition AS0 := Angle Uu Oo Uu.

Definition Ww : Point.
Proof.
destruct (CentralSymetPoint Uu Oo (sym_not_eq DistinctOoUu)) as (x,_).
exact x.
Defined.

Lemma DistOoWw : Distance Uu Oo = Distance Oo Ww.
Proof.
unfold Ww; destruct (CentralSymetPoint Uu Oo (sym_not_eq DistinctOoUu)).
intuition.
Qed.

Lemma DistinctOoWw : Oo <> Ww.
Proof.
apply (EquiDistantDistinct Oo Uu Oo Ww DistinctOoUu).
rewrite <- DistOoWw; apply DistSym.
Qed.

Lemma BetweenUuOoWw : Between Uu Oo Ww.
Proof.
unfold Ww; destruct (CentralSymetPoint Uu Oo (sym_not_eq DistinctOoUu)).
intuition.
Qed.

Lemma BetweenWwOoUu : Between Ww Oo Uu.
Proof.
assert (H := BetweenUuOoWw).
generalizeChange.
destruct (ClockwiseExists Uu Oo H0) as (V, H4).
elim (ClockwiseDistinctAB Oo Ww V); auto.
Qed.

Definition ASpi := Angle Uu Oo Ww.

Lemma NullAngle : forall A B C : Point,
A <> B ->
HalfLine A B C ->
Angle B A C = AS0.
Proof.
intros; unfold AS0 in |- *.
destruct (ExistsHalfLineEquidistant A B Oo Uu H DistinctOoUu) as (D, (H1, H2)).
rewrite (CongruentItself A B C D D H).
assert (H3 := EquiDistantDistinct Oo Uu A D DistinctOoUu (sym_eq H2)).
apply CongruentSSS; auto.
exact (DistAA D Uu).
canonize.
destruct (ClockwiseExists A B H) as (E, H4).
elim (ClockwiseDistinctAB A C E); auto.
trivial.
generalizeChange.
Qed.

Lemma ElongatedAngle : forall A B C : Point,
Between A B C ->
Angle A B C = ASpi.
Proof.
intros; unfold ASpi in |- *.
assert (H0 : B <> A).
canonize.
assert (H1 : B <> C).
canonize.
destruct (ClockwiseExists A B H2) as (D, H4).
elim (ClockwiseDistinctAB B C D); auto.
destruct (ExistsHalfLineEquidistant B A Oo Ww H0 DistinctOoWw)
as (D, (H2, H3)).
destruct (ExistsHalfLineEquidistant B C Oo Uu H1 DistinctOoUu)
as (E, (H4, H5)).
rewrite (CongruentItself B A C D E H0 H1 H2 H4).
apply CongruentSSS; auto.
canonize.
destruct (ClockwiseExists B C H1) as (F, H9).
elim (ClockwiseDistinctAB B E F); auto.
canonize.
destruct (ClockwiseExists B A H0) as (F, H9).
elim (ClockwiseDistinctAB B D F); auto.
rewrite <- (Chasles E B D).
rewrite (DistSym E B); rewrite H5; rewrite (DistSym Oo Uu).
rewrite H3; apply Chasles.
apply BetweenHalfLine; apply BetweenUuOoWw.
apply BetweenHalfLine; apply BetweenWwOoUu.
apply BetweenHalfLine; generalizeChange.
destruct (ClockwiseExists B C H1) as (F, H16).
elim (ClockwiseDistinctAB B E F); auto.
apply BetweenHalfLine; generalizeChange.
destruct (ClockwiseExists A B H6) as (F, H16).
elim (ClockwiseDistinctAB D B F); auto.
Qed.

Lemma NullAngleHalfLine : forall A B C : Point,
A <> B ->
A <> C ->
Angle B A C = AS0 ->
HalfLine A B C.
Proof.
intros.
destruct (ExistsHalfLineEquidistant A B A C H H0) as (D, (H2, H3)).
rewrite (DistNull C D).
trivial.
rewrite <- (NullDist C).
apply (CongruentSAS A C D A C C); auto.
apply (EquiDistantDistinct A C A D); auto.
rewrite <- (HalfLineAngleC A C B D); auto.
rewrite <- (AngleSym A B C); auto.
rewrite (NullAngle A C C); auto.
canonize.
Qed.

Lemma ElongatedAngleChasles : forall A B C : Point,
A <> B ->
A <> C ->
Angle B A C = ASpi ->
LSplus (Distance B A) (Distance A C) = Distance B C.
Proof.
intros.
destruct (ExistsBetweenEquidistant A C A B H0 H) as (D, (H2, H3)).
rewrite (DistSym B A); rewrite <- H3; rewrite (DistSym A D).
apply trans_eq with (y := Distance D C).
apply Chasles.
apply BetweenHalfLine; trivial.
apply BetweenSymHalfLine; trivial.
apply sym_eq; apply (CongruentSAS A B C A D C); auto.
rewrite (ElongatedAngle D A C); auto.
Qed.

Lemma ElongatedAngleRec : forall A B C : Point,
A <> B ->
A <> C ->
Angle B A C = ASpi ->
Between B A C.
Proof.
intros.
assert (H2 := ElongatedAngleChasles A B C H H0 H1).
destruct (ChaslesRec _ _ _ H2).
generalizeChange.
Qed.

End PARTICULAR_ANGLES.