Require Export D5_ParalleleConst.

Section SUM_ANGLES_PROPERTIES.

Lemma SumAnglesRec : forall A B C D E : Point,
        Clockwise A B C ->
        Clockwise A C D ->
        Between B A E ->
        Angle B A C = Angle A C D ->
        Angle D A E = Angle A D C.
Proof.
        intros.
        destruct (ExistsCongruentStrictTriangle D A C A D) as (F, (H3, H4)).
         autoClockwise.
         autoDistance.
         rewrite (CongruentStrictTrianglesA _ _ _ _ _ _ H3).
           apply HalfLineAngleC.
          autoDistinct.
          apply (BetweenDistinctBC _ _ _ H1).
          assert (H5 : Between B A F).
           apply (SumAngles A B C D F H H0 H4 H2).
             rewrite (CongruentStrictTrianglesA _ _ _ _ _ _ H3); trivial.
           assert (H6 := EquiOrientedRev _ _ _ H1); canonize.
Qed.

Lemma SumAnglesCorollary : forall A B C D E A' B' C' : Point,
        Clockwise A' B' C' ->
        Clockwise A B C ->
        Clockwise A C D ->
        Angle B A C = Angle A' B' C' ->
        Angle C A D = Angle B' A' C' ->
        Between B A E ->
        Angle D A E = Angle A' C' B'.
Proof.
        intros.
        destruct (ExistsHalfLineEquidistant A C A' B') as (B'', (H6, H7)).
         autoDistinct.
         autoDistinct.
         destruct (ExistsHalfLineEquidistant A D A' C') as (C'', (H8, H9)).
          autoDistinct.
          autoDistinct.
          assert (H10 : CongruentStrictTriangles A' B' C' A B'' C'').
           apply CongruentStrictTrianglesSASA.
            auto.
            auto.
            rewrite <- H3; apply HalfLineAngleBC.
             autoDistinct.
             autoDistinct.
             trivial.
             trivial.
            exact (ClockwiseNotCollinear _ _ _ H).
           rewrite (CongruentStrictTrianglesC _ _ _ _ _ _ H10).
             rewrite (HalfLineAngleB A D E C'').
            apply (SumAnglesRec A B).
             apply ClockwiseBCA; generalizeChangeSense.
               apply H4; autoClockwise.
             generalizeChangeSense.
               apply H6; apply ClockwiseBCA; apply H12; autoClockwise.
             trivial.
             rewrite <- (CongruentStrictTrianglesB _ _ _ _ _ _ H10); rewrite <- H2.
               apply HalfLineAngleC.
              autoDistinct.
              apply (HalfLineDistinct A C B'').
               autoDistinct.
               trivial.
              apply HalfLineSym.
               autoDistinct.
               trivial.
            autoDistinct.
            exact (BetweenDistinctBC _ _ _ H4).
            trivial.
Qed.

Lemma TwoEmbeddedTriangles : forall A B C D E : Point,
        Clockwise A B C ->
        Between A D B ->
        Between A E C ->
        Angle A D E = Angle A B C ->
        Angle A E D = Angle A C B.
Proof.
        intros.
        destruct (ExistsDParallelogramm _ _ _ (ClockwiseBCA _ _ _ H)) as (F, H3).
        destruct
         (CentralSymetPoint F A (sym_not_eq (ParallelogrammDistinctCD _ _ _ _ H3)))
         as (G, (_, H4)).
        rewrite <- (SumAnglesRec A F B C G).
         rewrite <- (SumAnglesRec A F D E G).
          apply BetweenAngleB.
           exact (BetweenDistinctBC _ _ _ H4).
           trivial.
          apply ClockwiseBCA; apply (BetweenClockwiseMBC B A F D).
           apply ClockwiseCAB;
            apply
             (ParallelogrammClockwiseBCD _ _ _ _ (ParallelogrammPermut _ _ _ _ H3)).
           exact (BetweenSym _ _ _ H0).
          exact (TriangleAMN A B C D E H H0 H1).
          trivial.
          rewrite (BetweenAngleC A F D B).
           rewrite H2; assert (H5 := ParallelogrammCongruentTrianglesAC _ _ _ _ H3).
             rewrite <- (CongruentStrictTrianglesA _ _ _ _ _ _ H5).
             apply AngleSym; autoDistinct.
           apply sym_not_eq; exact (BetweenDistinctAB _ _ _ H4).
           trivial.
         apply (ParallelogrammClockwiseBCD _ _ _ _ (ParallelogrammPermut _ _ _ _ H3)).
         trivial.
         trivial.
         assert (H5 := ParallelogrammCongruentTrianglesAC _ _ _ _ H3).
           rewrite <- (CongruentStrictTrianglesA _ _ _ _ _ _ H5).
           apply AngleSym; autoDistinct.
Qed.

Lemma TwoEmbeddedSymTriangles : forall A B C D E : Point,
        Clockwise A B C ->
        Between A D B ->
        Between A E C ->
        Angle A E D = Angle A C B ->
        Angle A D E = Angle A B C.
Proof.
        intros.
        destruct (ExistsHalfLineEquidistant A C A B) as (B', (H3, H4)).
         autoDistinct.
         autoDistinct.
         destruct (ExistsHalfLineEquidistant A B A C) as (C', (H5, H6)).
          autoDistinct.
          autoDistinct.
          assert (H7 := TriangleAMN A B C D E H H0 H1).
            destruct (ExistsHalfLineEquidistant A E A D) as (D', (H8, H9)).
           autoDistinct.
           autoDistinct.
           destruct (ExistsHalfLineEquidistant A D A E) as (E', (H10, H11)).
            autoDistinct.
            autoDistinct.
            assert (H12 : CongruentStrictTriangles A B C A B' C').
             apply CongruentStrictTrianglesSASA.
              auto.
              auto.
              apply CongruentItself; autoDistinct.
              exact (ClockwiseNotCollinear _ _ _ H).
             assert (H13 : CongruentStrictTriangles A D E A D' E').
              apply CongruentStrictTrianglesSASA.
               auto.
               auto.
               apply CongruentItself; autoDistinct.
               exact (ClockwiseNotCollinear _ _ _ H7).
              rewrite (CongruentStrictTrianglesB _ _ _ _ _ _ H12).
                rewrite (CongruentStrictTrianglesB _ _ _ _ _ _ H13).
                apply TwoEmbeddedTriangles.
               generalizeChangeSense.
                 apply H5; apply ClockwiseBCA.
                 apply H1; autoClockwise.
               apply LSltBetween.
                apply (HalfLineDistinct A D); [ autoDistinct | auto ].
                assert (H14 := BetweenHalfLine _ _ _ H0).
                  canonize.
                  apply H5; apply H14.
                  clear H3 H5 H8 H14 H16 H17; generalizeChange.
                rewrite H11; rewrite H6; exact (BetweenLSlt _ _ _ H1).
               apply LSltBetween.
                apply (HalfLineDistinct A E); [ autoDistinct | auto ].
                assert (H14 := BetweenHalfLine _ _ _ H1).
                  canonize.
                  apply H3; apply H14.
                  clear H3 H5 H10 H14 H16 H17; generalizeChange.
                rewrite H9; rewrite H4; exact (BetweenLSlt _ _ _ H0).
               rewrite <- (CongruentStrictTrianglesC _ _ _ _ _ _ H12).
                 rewrite <- (CongruentStrictTrianglesC _ _ _ _ _ _ H13).
                 trivial.
Qed.

Lemma ExternParallelogramm : forall A B C D E : Point,
        Parallelogramm A B C D ->
        Between D C E ->
        Angle A B C = Angle B C E.
Proof.
        intros.
        rewrite (AngleSym B).
         apply sym_eq; apply (SumAnglesRec C D A B E).
          apply (ParallelogrammClockwiseBCD _ _ _ _ (ParallelogrammPermut _ _ _ _ H)).
          apply (ParallelogrammClockwiseBDA _ _ _ _ (ParallelogrammPermut _ _ _ _ H)).
          trivial.
          rewrite (AngleSym A).
           apply sym_eq; apply CongruentStrictTrianglesA.
             exact (ParallelogrammCongruentTrianglesAC _ _ _ _ H).
           exact (ParallelogrammDistinctAC _ _ _ _ H).
           exact (ParallelogrammDistinctAB _ _ _ _ H).
         exact (sym_not_eq (ParallelogrammDistinctAB _ _ _ _ H)).
         exact (ParallelogrammDistinctAB _ _ _ _ (ParallelogrammPermut _ _ _ _ H)).
Qed.

Lemma ExternOppParallelogramm : forall A B C D E : Point,
        Parallelogramm A B C D ->
        Between B C E ->
        Angle A B C = Angle D C E.
Proof.
        intros.
        destruct (CentralSymetPoint D C) as (F, (H1, H2)).
         apply sym_not_eq; exact (ParallelogrammDistinctCD _ _ _ _ H).
         rewrite (ExternParallelogramm _ _ _ _ _ H H2).
           apply CongruentOpp.
          trivial.
          exact (BetweenSym _ _ _ H2).
          apply ClockwiseNotCollinear.
            apply ClockwiseBCA; apply (EquiOrientedRev _ _ _ (BetweenSym _ _ _ H2)).
            canonize; apply ClockwiseBCA;
             exact (ParallelogrammClockwiseBCD _ _ _ _ H).
Qed.

Lemma ParallelogrammExtern : forall A B C D E : Point,
        Parallelogramm A B C D ->
        Clockwise C B E ->
        Angle A B C = Angle B C E ->
        Between D C E.
Proof.
        intros.
        apply (SumAngles C D A B E).
         exact (ParallelogrammClockwiseBCD _ _ _ _ (ParallelogrammPermut _ _ _ _ H)).
         exact (ParallelogrammClockwiseBDA _ _ _ _ (ParallelogrammPermut _ _ _ _ H)).
         trivial.
         assert (H2 := ParallelogrammCongruentTrianglesAC _ _ _ _ H).
           apply sym_eq; rewrite (AngleSym A).
          exact (CongruentStrictTrianglesA _ _ _ _ _ _ H2).
          exact (ParallelogrammDistinctAC _ _ _ _ H).
          exact (ParallelogrammDistinctAB _ _ _ _ H).
         rewrite (AngleSym B); auto.
          autoDistinct.
          exact (sym_not_eq (ParallelogrammDistinctAB _ _ _ _ H)).
Qed.

End SUM_ANGLES_PROPERTIES.