# Library RulerCompassGeometry.E3_Congruence

Require Export E2_Ordre.

Section CONGRUENCE.

Lemma C1a : forall A B C D : Point,
A <> B ->
C <> D ->
exists E : Point, HalfLine C D E /\ Distance A B = Distance C E.
Proof.
intros.
destruct (ExistsHalfLineEquidistant C D A B) as (E, (H1, H2)); auto.
exists E; intuition.
Qed.

Lemma C1b : forall A B C D E F : Point,
A <> B ->
C <> D ->
HalfLine C D E ->
Distance A B = Distance C E ->
HalfLine C D F ->
Distance A B = Distance C F ->
E = F.
Proof.
intros.
setLine C D H0 ipattern:L ipattern:CD.
setCircle C A B H ipattern:G ipattern:CAB.
setLinterposC L G CD CAB ipattern:J ipattern:H5 ipattern:H6 ipattern:H7
ipattern:H8.
autoCollinear.
apply trans_eq with (y := J).
apply sym_eq; apply H8.
split.
apply HalfLineCollinear; trivial.
split.
autoDistance.
canonize.
apply H8; split.
apply HalfLineCollinear; trivial.
split.
autoDistance.
canonize.
Qed.

Lemma C2a : forall A B C D E F : Point,
Distance A B = Distance C D ->
Distance A B = Distance E F ->
Distance C D = Distance E F.
Proof.
intros A B C D E F H H0; rewrite <- H; auto.
Qed.

Lemma C2b : forall A B : Point,
Distance A B = Distance A B.
Proof.
auto.
Qed.

Lemma C3 : forall A B C D E F : Point,
Between A B C ->
Between D E F ->
Distance A B = Distance D E ->
Distance B C = Distance E F ->
Distance A C = Distance D F.
Proof.
intros; rewrite <- (Chasles A B C).
rewrite H1; rewrite H2; apply Chasles; auto.
apply BetweenHalfLine; trivial.
apply BetweenSymHalfLine; trivial.
apply BetweenHalfLine; trivial.
apply BetweenSymHalfLine; trivial.
Qed.

Lemma C4a : forall A B C D F : Point,
A <> B ->
A <> C ->
D <> F ->
exists E : Point,
D <> E /\
~Clockwise D F E /\
Angle B A C = Angle E D F.
Proof.
intros; decompose [or] (ExclusiveFourCases A B C H0).
destruct (ExistsHalfLineEquidistant D F A B H1 H) as (G, (H3, H4)).
destruct (EqualTriangleAntiClockwise A B C D G) as (E, (H5, (H6, H7)));
auto.
assert (H8 := ClockwiseDistinctAB D E G H5); exists E; intuition.
elim (ClockwiseNotClockwise D E G H5); apply ClockwiseCAB; canonize.
rewrite (CongruentItself D E F E G); canonize.
apply CongruentSSS; autoDistance.
destruct (ExistsHalfLineEquidistant D F A C H1 H0) as (G, (H2, H4)).
destruct (EqualTriangleAntiClockwise A C B D G) as (E, (H5, (H6, H7))).
autoClockwise.
auto.
assert (H8 := ClockwiseDistinctAB D E G H5); exists E; intuition.
elim (ClockwiseNotClockwise D E G H5); apply ClockwiseCAB; canonize.
rewrite (HalfLineAngleC D E F G); canonize.
apply CongruentSSS; autoDistance.
exists F; intuition.
autoClockwise.
rewrite (NullAngle D F F); canonize.
apply NullAngle; auto.
destruct (CentralSymetPoint F D (sym_not_eq H1)) as (E, (H3, H4)).
exists E; intuition.
elim (BetweenDistinctBC F D E H4); trivial.
elim (BetweenNotClockwiseBAC F D E H4); trivial.
rewrite (ElongatedAngle E D F (BetweenSym F D E H4)).
apply ElongatedAngle; split.
auto.
apply EquiOrientedSym; generalizeChangeSide.
Qed.

Lemma C4b : forall A B C D F : Point,
A <> B ->
A <> C ->
D <> F ->
exists E : Point,
D <> E /\
~Clockwise D E F /\
Angle B A C = Angle E D F.
Proof.
intros; decompose [or] (ExclusiveFourCases A B C H0).
destruct (ExistsHalfLineEquidistant D F A B H1 H) as (G, (H3, H4)).
destruct (EqualTriangleClockwise A B C D G) as (E, (H5, (H6, H7))); auto.
assert (H8 := ClockwiseDistinctCA D G E H5); exists E; intuition.
generalizeChangeSense; elim (ClockwiseNotClockwise D G E H5).
apply H10; autoClockwise.
rewrite (CongruentItself D E F E G); canonize.
apply CongruentSSS; autoDistance.
destruct (ExistsHalfLineEquidistant D F A C H1 H0) as (G, (H2, H4)).
destruct (EqualTriangleClockwise A C B D G) as (E, (H5, (H6, H7))).
autoClockwise.
auto.
assert (H8 := ClockwiseDistinctCA D G E H5); exists E; intuition.
generalizeChangeSense; elim (ClockwiseNotClockwise D G E H5).
apply H10; autoClockwise.
rewrite (HalfLineAngleC D E F G); canonize.
apply CongruentSSS; autoDistance.
exists F; intuition.
autoClockwise.
rewrite (NullAngle D F F); canonize.
apply NullAngle; auto.
destruct (CentralSymetPoint F D (sym_not_eq H1)) as (E, (H3, H4)).
exists E; intuition.
elim (BetweenDistinctBC F D E H4); trivial.
elim (BetweenNotClockwiseABC F D E H4); autoClockwise.
rewrite (ElongatedAngle E D F (BetweenSym F D E H4)).
apply ElongatedAngle; split.
auto.
apply EquiOrientedSym; generalizeChangeSide.
Qed.

Lemma C4c : forall A B C D F E E' : Point,
A <> B ->
A <> C ->
D <> F ->
D <> E ->
D <> E' ->
~Clockwise D E F ->
~Clockwise D E' F ->
Angle B A C = Angle E D F ->
Angle B A C = Angle E' D F ->
Superimposed (HalfLine D E) (HalfLine D E').
Proof.
intros.
apply SuperimposedHalfLines; auto.
apply (EqualAngleHalfLineB D E E' F); auto.
rewrite <- H6; auto.
Qed.

Lemma C4d : forall A B C D F E E' : Point,
A <> B ->
A <> C ->
D <> F ->
D <> E ->
D <> E' ->
~Clockwise D F E ->
~Clockwise D F E' ->
(Angle B A C) = (Angle E D F) ->
(Angle B A C) = (Angle E' D F) ->
Superimposed (HalfLine D E) (HalfLine D E').
Proof.
intros.
apply SuperimposedHalfLines; auto.
apply (EqualAngleHalfLineC D F E E'); auto.
rewrite <- H6; auto.
Qed.

Lemma C5a : forall A B C : Point,
Angle B A C = Angle B A C.
Proof.
trivial.
Qed.

Lemma C5b : forall A B C D E F G H J : Point,
Angle B A C = Angle E D F ->
Angle B A C = Angle H G J ->
Angle E D F = Angle H G J.
Proof.
intros.
rewrite <- H0; trivial.
Qed.

Lemma C6a : forall A B C D E F : Point,
A <> B ->
A <> C ->
Distance A B = Distance D E ->
Distance A C = Distance D F ->
Angle B A C = Angle E D F ->
Distance B C = Distance E F.
Proof.
intros; apply (CongruentSAS A B C D E F); auto.
Qed.

Lemma C6b : forall A B C D E F : Point,
A <> B ->
A <> C ->
B <> C ->
Distance A B = Distance D E ->
Distance A C = Distance D F ->
Angle B A C = Angle E D F ->
Angle A B C = Angle D E F.
Proof.
intros.
apply CongruentSSS; auto.
rewrite (DistSym B A); rewrite (DistSym E D); trivial.
apply (CongruentSAS A B C D E F); auto.
Qed.

Lemma C6c : forall A B C D E F : Point,
A <> B ->
A <> C ->
B <> C ->
Distance A B = Distance D E ->
Distance A C = Distance D F ->
Angle B A C = Angle E D F ->
Angle A C B = Angle D F E.
Proof.
intros.
apply CongruentSSS; auto.
rewrite (DistSym C A); rewrite (DistSym F D); trivial.
rewrite (DistSym C B); rewrite (DistSym F E).
apply (CongruentSAS A B C D E F); auto.
Qed.

End CONGRUENCE.