Library GeoCoq.Tarski_dev.Ch13_4_cos


Require Export GeoCoq.Tarski_dev.Ch13_3_angles.

Ltac anga_instance_o a A B P C :=
        assert(tempo_anga:= anga_const_o a A B P);
        match goal with
           |H: Q_CongA_Acute a |- _assert(tempo_H:= H); apply tempo_anga in tempo_H; ex_elim tempo_H C
        end;
        clear tempo_anga.

Section Cosinus.

Context `{T2D:Tarski_2D}.


Definition Lcos lb lc a :=
  Q_Cong lb Q_Cong lc Q_CongA_Acute a
  ( A, B, C, (Per C B A lb A B lc A C a B A C)).

Lemma l13_6 : a lc ld l, Lcos lc l a Lcos ld l a EqL lc ld.
Proof.
    intros.
    unfold Lcos in ×.
    spliter.
    ex_and H6 X1.
    ex_and H7 Y1.
    ex_and H6 Z1.
    ex_and H3 X2.
    ex_and H10 Y2.
    ex_and H3 Z2.
    clean_duplicated_hyps.
    assert(Len X1 Z1 l).
      split; auto.
    assert(Len X2 Z2 l).
      split; auto.
    assert(Cong X1 Z1 X2 Z2).
      eapply (is_len_cong _ _ _ _ l); auto.
    assert(Ang_Acute Y1 X1 Z1 a).
      split; auto.
    assert(Ang_Acute Y2 X2 Z2 a).
      split; auto.
    assert(CongA Y1 X1 Z1 Y2 X2 Z2).
      apply (is_anga_conga _ _ _ _ _ _ a); split; auto.
    assert(Len X1 Y1 lc).
      split; auto.
    assert(Len X2 Y2 ld).
      split; auto.
    induction(eq_dec_points Z1 Y1).
      subst Z1.
      assert(Out X2 Y2 Z2).
        apply (eq_conga_out Y1 X1); auto.
      assert(Y2 = Z2).
        assert(Z2 = Y2 X2 = Y2).
          apply l8_9.
            auto.
          apply out_col in H19.
          Col.
        induction H20.
          auto.
        unfold Out in H19.
        spliter.
        subst Y2.
        tauto.
      subst Z2.
      assert(EqL l lc).
        apply ex_eql.
         X1.
         Y1.
        split; auto.
      assert(EqL l ld).
        apply ex_eql.
         X2.
         Y2.
        split; auto.
     transitivity l;auto.
     symmetry; auto.
    assert(Z2 Y2).
      intro.
      subst Z2.
      assert(Out X1 Y1 Z1).
        apply (eq_conga_out Y2 X2).
        apply conga_sym.
        auto.
      assert(Y1 = Z1).
        assert(Z1 = Y1 X1 = Y1).
          apply l8_9.
            auto.
          apply out_col in H20.
          Col.
        induction H21.
          auto.
        subst Y1.
        unfold Out in H20.
        spliter.
        tauto.
      subst Z1.
      tauto.
    apply conga_distinct in H16.
    spliter.
    assert(CongA X1 Y1 Z1 X2 Y2 Z2).
      apply l11_16; Perp; auto.
    assert(¬Col Z1 X1 Y1).
      intro.
      assert(X1 = Y1 Z1 = Y1).
        apply l8_9.
          Perp.
        Col.
      induction H27.
        subst Y1.
        tauto.
      contradiction.
    apply conga_comm in H16.
    apply cong_commutativity in H13.
    assert(HH:=l11_50_2 Z1 X1 Y1 Z2 X2 Y2 H26 H25 H16 H13).
    spliter.
    apply ex_eql.
     X1.
     Y1.
    split.
      auto.
    eapply is_len_cong_is_len.
      apply H18.
    Cong.
Qed.

Lemma null_lcos_eql : lp l a, Lcos lp l a Q_CongA_Null_Acute a EqL l lp.
Proof.
    intros.
    unfold Lcos in H.
    spliter.
    ex_and H3 A.
    ex_and H4 B.
    ex_and H3 C.
    unfold Q_CongA_Null_Acute in H0.
    spliter.
    assert(HH:= H7 B A C H6).
    assert(Col A B C) by (apply out_col;auto).
    assert(Col C B A) by Col.
    assert(HQ:= l8_9 C B A H3 H9).
    induction HQ.
      subst C.
      apply (all_eql A B).
        split; auto.
      split; auto.
    subst B.
    exfalso.
    unfold Out in HH.
    tauto.
Qed.

Lemma eql_lcos_null : l lp a, Lcos l lp a EqL l lp Q_CongA_Null_Acute a.
Proof.
    intros.
    unfold Lcos in H.
    spliter.
    ex_and H3 B.
    ex_and H4 A.
    ex_and H3 C.
    assert( A0 B0 : Tpoint, l A0 B0 lp A0 B0).
      apply H0; auto.
    assert(HP:= (H7 B A)).
    assert(HQ:= (H7 B C)).
    destruct HP.
    destruct HQ.
    assert(l B C).
      apply H11.
      auto.
    assert(lp B A).
      apply H8.
      auto.
    clear H7 H8 H9 H10 H11.
    assert(Cong B A B C).
      apply (lg_cong l); auto.
    unfold Per in H3.
    ex_and H3 B'.
    assert(HH:= anga_distinct a A B C H2 H6).
    spliter.
    assert(A = C).
      eapply (l4_18 B B').
        intro.
        subst B'.
        apply l7_3 in H3.
        contradiction.
        unfold Midpoint in H3; assert(HH:= midpoint_col).
        spliter.
        apply bet_col in H3.
        Col.
        auto.
      unfold Midpoint in H3.
      spliter.
      eapply cong_transitivity.
        apply cong_symmetry.
        apply cong_commutativity.
        apply H11.
      eapply cong_transitivity.
        apply cong_commutativity.
        apply H7.
      Cong.
    subst C.
    unfold Q_CongA_Null_Acute.
    split.
      auto.
    intros A0 B0 C0 HP.
    apply (eq_conga_out A B).
    apply (anga_conga a); auto.
Qed.

Lemma lcos_lg_not_null: l lp a, Lcos l lp a ¬ Q_Cong_Null l ¬ Q_Cong_Null lp.
Proof.
    intros.
    unfold Lcos in H.
    spliter.
    ex_and H2 A.
    ex_and H3 B.
    ex_and H2 C.
    assert(HH:= anga_distinct a B A C H1 H5).
    spliter.
    unfold Q_Cong_Null.
    split; intro; spliter; ex_and H9 X.
      assert (Cong A B X X) by (apply (lg_cong l); auto).
      treat_equalities;intuition.
    assert(Cong A C X X) by (apply (lg_cong lp); auto).
    treat_equalities;intuition.
Qed.

Lemma perp_acute_out : A B C C', Acute A B C Perp A B C C' Col A B C' Out B A C'.
Proof.
    intros.
    assert (HH:= H).
    unfold Acute in HH.
    ex_and HH A0.
    ex_and H2 B0.
    ex_and H3 C0.
    assert(HH:=H3).
    unfold LtA in HH.
    spliter.
    unfold LeA in H4.
    ex_and H4 P0.
    apply conga_distinct in H6.
    spliter.
    assert(C' B).
      intro.
      subst C'.
      assert(Per A B C).
        apply perp_in_per.
        apply perp_in_comm.
        apply perp_perp_in; auto.
        Perp.
      unfold InAngle in H4.
      spliter.
      apply H5.
      apply l11_16; auto.
    induction H1.
      apply False_ind.
      assert(HH:= H4).
      unfold InAngle in HH.
      spliter.
      ex_and H15 X.
      induction H16.
        subst X.
        assert(¬ Col A0 B0 C0).
          apply per_not_col; auto.
        assert(Col A0 B0 C0).
          apply bet_col.
          auto.
        contradiction.
      assert(LeA A B C A0 B0 C0).
        unfold LtA in H3.
        spliter.
        auto.
      assert(HQ:= l11_29_a A B C A0 B0 C0 H17).
      ex_and HQ Q.
      assert(Per A B Q).
        apply (l11_17 A0 B0 C0).
          auto.
        apply conga_sym.
        auto.
      assert(Perp_at B Q B A B).
        apply perp_in_right_comm.
        apply per_perp_in.
          apply conga_distinct in H19.
          spliter.
          auto.
          auto.
        apply l8_2.
        auto.
      assert(HH:= perp_in_perp_bis Q B A B B H21).
      induction HH.
        apply perp_distinct in H22.
        tauto.
      assert(HH:= l12_9 Q B C C' A B).
      assert(Par Q B C C').
        apply HH; Perp.
      assert(OS B Q C C').
        apply l12_6.
        induction H23.
          apply par_strict_left_comm.
          auto.
        spliter.
        apply False_ind.
        assert(¬Col B C' C).
          apply per_not_col; auto.
          apply perp_in_per.
          apply perp_in_comm.
          apply perp_perp_in.
          apply perp_comm.
          apply (perp_col _ A); Perp.
          apply bet_col in H1.
          Col.
        apply H27.
        Col.
      assert(OS Q B C A).
        eapply in_angle_one_side.
          intro.
          assert(¬ Col B Q A).
            apply( perp_not_col).
            Perp.
          apply H26.
          Col.
          intro.
          apply H11.
          eapply (l8_18_uniqueness A B Q).
            intro.
            assert(¬Col B A Q).
              apply perp_not_col.
              Perp.
            apply H27.
            Col.
            apply bet_col in H1.
            Col.
            apply perp_sym.
            apply perp_left_comm.
            eapply (perp_col _ C).
              intro.
              subst Q.
              unfold OS in H24.
              ex_and H24 T.
              unfold TS in H26.
              spliter.
              apply H26.
              Col.
              Perp.
            unfold Par in H23.
            induction H23.
              apply False_ind.
              apply H23.
               C.
              split; Col.
            spliter.
            Col.
            Col.
          Perp.
        apply l11_24.
        auto.
      apply invert_one_side in H25.
      assert(OS B Q A C').
        eapply one_side_transitivity.
          apply one_side_symmetry.
          apply H25.
        assumption.
      assert(¬ Col B A Q).
        apply perp_not_col.
        Perp.
      assert(TS B Q A C').
        unfold TS.
        repeat split; auto.
          apply perp_distinct in H22.
          spliter.
          auto.
          intro.
          apply H27.
          Col.
          intro.
          apply H27.
          apply bet_col in H1.
          ColR.
         B.
        split.
          Col.
        auto.
      apply l9_9_bis in H26.
      contradiction.
    unfold Out.
    repeat split; auto.
    induction H1.
      right.
      auto.
    left.
    Between.
Qed.

End Cosinus.

Section Cosinus2.

Context `{T2D:Tarski_2D}.

Lemma perp_out__acute : A B C C', Perp A B C C' Col A B C' (Acute A B C Out B A C').
Proof.
    intros.
    split.
      intro.
      apply (perp_acute_out _ _ C); auto.
    intro.
    apply (perp_out_acute _ _ C C'); auto.
Qed.

Lemma obtuse_not_acute : A B C, Obtuse A B C ¬ Acute A B C.
Proof.
    intros.
    intro.
    unfold Obtuse in H.
    unfold Acute in H0.
    ex_and H A0.
    ex_and H1 B0.
    ex_and H C0.
    ex_and H0 A1.
    ex_and H2 B1.
    ex_and H0 C1.
    assert(A0 B0 C0 B0 A1 B1 C1 B1 A B C B).
      unfold GtA in H1.
      unfold LtA in ×.
      unfold LeA in ×.
      spliter.
      ex_and H1 P0.
      ex_and H2 P.
      unfold InAngle in H2.
      unfold CongA in H5 .
      unfold CongA in H6 .
      spliter.
      repeat split; auto.
    spliter.
    assert(CongA A0 B0 C0 A1 B1 C1).
      apply l11_16; auto.
    assert(GtA A B C A1 B1 C1).
      apply (conga_preserves_gta A B C A0 B0 C0).
        apply conga_refl; auto.
        auto.
      assumption.
    assert(HH:=not_lta_and_gta A B C A1 B1 C1).
    apply HH.
    split; auto.
Qed.

Lemma acute_not_obtuse : A B C, Acute A B C ¬ Obtuse A B C.
Proof.
    intros.
    intro.
    apply obtuse_not_acute in H0.
    contradiction.
Qed.

Lemma perp_obtuse_bet : A B C C', Perp A B C C' Col A B C' Obtuse A B C Bet A B C'.
Proof.
    intros.
    assert(HH:= H1).
    unfold Obtuse in HH.
    ex_and HH A0.
    ex_and H2 B0.
    ex_and H3 C0.
    assert(A0 B0 C0 B0 A B C B).
      unfold GtA in H3.
      unfold LtA in H3.
      spliter.
      unfold LeA in H3.
      ex_and H3 P.
      unfold CongA in H5.
      spliter.
      repeat split; auto.
      intro.
      subst C.
      apply perp_comm in H.
      apply perp_not_col in H.
      apply H.
      Col.
    spliter.
    assert(B C').
      intro.
      subst C'.
      assert(Per A B C).
        apply perp_in_per.
        apply perp_in_comm.
        apply perp_perp_in.
        Perp.
      assert(CongA A0 B0 C0 A B C).
        apply l11_16; auto.
      unfold GtA in H3.
      unfold LtA in H3.
      spliter.
      unfold LeA in H3.
      contradiction.
    induction H0.
      auto.
    assert(Out B A C').
      unfold Out.
      repeat split; auto.
      induction H0.
        right.
        auto.
      left.
      Between.
    eapply (perp_out_acute _ _ C) in H9.
      apply obtuse_not_acute in H1.
      contradiction.
      auto.
Qed.

Lemma lcos_const0 : l lp a, Lcos lp l a Q_CongA_Null_Acute a
  A, B, C, l A B lp B C a A B C.
Proof.
    intros.
    assert(HH:=H).
    unfold Lcos in HH.
    spliter.
    ex_and H4 A.
    ex_and H5 B.
    ex_and H4 C.
     C.
     A.
     B.
    repeat split.
      apply lg_sym; auto.
      auto.
    apply anga_sym; auto.
Qed.

Lemma lcos_const1 : l lp a P, Lcos lp l a ¬ Q_CongA_Null_Acute a
  A, B, C, ¬Col A B P OS A B C P l A B lp B C a A B C.
Proof.
    intros.
    assert(HH:=H).
    unfold Lcos in HH.
    spliter.
    assert(HH:= (lcos_lg_not_null lp l a H)).
    spliter.
    lg_instance_not_col l P A B.
     A.
     B.
    assert(HH:=anga_const_o a A B P H8 H0 H3).
    ex_and HH C'.
    assert(A B B C').
      assert(HP:= anga_distinct a A B C' H3 H9).
      spliter.
      auto.
    spliter.
    assert(HH:=ex_point_lg_out lp B C' H12 H1 H5).
    ex_and HH C.
     C.
    repeat split; auto.
      assert(¬ Col A B C').
        unfold OS in H10.
        ex_and H10 D.
        unfold TS in H10.
        spliter.
        intro.
        apply H10.
        Col.
      assert(HP:=out_one_side_1 A B C' C B H11 H15).
      eapply (one_side_transitivity _ _ _ C').
        apply one_side_symmetry.
        apply HP.
          Col.
        apply l6_6.
        auto.
      auto.
    apply (anga_out_anga a A B C'); auto.
      apply out_trivial.
      auto.
    apply l6_6.
    auto.
Qed.

Lemma lcos_const : lp l a, Lcos lp l a
  A, B, C, lp A B l B C a A B C.
Proof.
    intros.
    unfold Lcos in H.
    spliter.
    ex_and H2 A.
    ex_and H3 B.
    ex_and H2 C.
     B.
     A.
     C.
    repeat split; auto.
    apply lg_sym; auto.
Qed.

Lemma lcos_lg_distincts : lp l a A B C, Lcos lp l a l A B lp B C a A B C A B C B.
Proof.
    intros.
    assert(HH:= lcos_lg_not_null lp l a H).
    spliter.
    unfold Q_Cong_Null in ×.
    split.
      intro.
      subst B.
      apply H4.
      unfold Lcos in H.
      split.
        tauto.
       A.
      auto.
    intro.
    subst C.
    apply H3.
    unfold Lcos in H.
    split.
      tauto.
     B.
    auto.
Qed.

Lemma lcos_const_a : lp l a B, Lcos lp l a A, C, l A B lp B C a A B C.
Proof.
    intros.
    assert(HH:=H).
    unfold Lcos in HH.
    spliter.
    clear H3.
    assert(HH:= ex_point_lg l B H1).
    ex_and HH A.
    assert(l A B).
      apply lg_sym; auto.
     A.
    assert(HH:= lcos_lg_not_null lp l a H).
    spliter.
    assert(A B).
      intro.
      subst A.
      apply H6.
      unfold Q_Cong_Null.
      split.
        auto.
       B.
      auto.
    assert(HH:= anga_const a A B H2 H7).
    ex_and HH C'.
    assert(HH:= anga_distincts a A B C' H2 H8).
    spliter.
    assert(B C'); auto.
    assert(HH:= ex_point_lg_out lp B C' H11 H0 H5).
    ex_and HH C.
     C.
    repeat split; auto.
    apply (anga_out_anga a A B C' A C); auto.
      apply out_trivial.
      auto.
    apply l6_6.
    auto.
Qed.

Lemma lcos_const_ab : lp l a B A, Lcos lp l a l A B C, lp B C a A B C.
Proof.
    intros.
    assert(HH:=H).
    unfold Lcos in HH.
    spliter.
    clear H4.
    assert(HH:= lcos_lg_not_null lp l a H).
    spliter.
    assert(A B).
      intro.
      subst A.
      apply H5.
      unfold Q_Cong_Null.
      split.
        auto.
       B.
      auto.
    assert(HH:= anga_const a A B H3 H6).
    ex_and HH C'.
    assert(HH:= anga_distincts a A B C' H3 H7).
    spliter.
    assert(B C'); auto.
    assert(HH:= ex_point_lg_out lp B C' H10 H1 H4).
    ex_and HH C.
     C.
    repeat split; auto.
    apply (anga_out_anga a A B C' A C); auto.
      apply out_trivial.
      auto.
    apply l6_6.
    auto.
Qed.

Lemma lcos_const_cb : lp l a B C, Lcos lp l a lp B C A, l A B a A B C.
Proof.
    intros.
    assert(HH:=H).
    unfold Lcos in HH.
    spliter.
    clear H4.
    assert(HH:= lcos_lg_not_null lp l a H).
    spliter.
    assert(C B).
      intro.
      subst C.
      apply H4.
      unfold Q_Cong_Null.
      split.
        auto.
       B.
      auto.
    assert(HH:= anga_const a C B H3 H6).
    ex_and HH A'.
    assert(HH:= anga_distincts a C B A' H3 H7).
    spliter.
    assert(B A'); auto.
    assert(HH:= ex_point_lg_out l B A' H10 H2 H5).
    ex_and HH A.
     A.
    split.
      apply lg_sym; auto.
    apply(anga_out_anga a A' B C); auto.
      apply anga_sym; auto.
      apply l6_6.
      auto.
    apply out_trivial.
    auto.
Qed.

Lemma lcos_lg_anga : l lp a, Lcos lp l a Lcos lp l a Q_Cong l Q_Cong lp Q_CongA_Acute a.
Proof.
    intros.
    split.
      auto.
    unfold Lcos in H.
    tauto.
Qed.

Lemma lcos_eql_lcos : lp1 l1 lp2 l2 a, EqL lp1 lp2 EqL l1 l2 Lcos lp1 l1 a Lcos lp2 l2 a.
Proof.
    intros.
    unfold Lcos in ×.
    spliter.
    ex_and H4 A.
    ex_and H5 B.
    ex_and H4 C.

    assert(HH:=lg_eql_lg l1 l2 H2 H0).
    assert(HP:=lg_eql_lg lp1 lp2 H1 H).
    repeat split; auto.
     A.
     B.
     C.
    unfold EqL in ×.
    spliter.
    repeat split; auto.
      apply H.
      auto.
    apply H0; auto.
Qed.

Require Export Morphisms.

Global Instance lcos_morphism :
 Proper (EqL ==> EqL ==> eq ==> iff) Lcos.
Proof.
unfold Proper.
split.
 - rewrite H1.
   intro.
   eauto using lcos_eql_lcos.
 - intro.
   rewrite H1.
   eapply lcos_eql_lcos with y y0;
   try symmetry;assumption.
Qed.

Lemma lcos_not_lg_null : lp l a, Lcos lp l a ¬ Q_Cong_Null lp.
Proof.
    intros.
    intro.
    unfold Q_Cong_Null in H0.
    spliter.
    unfold Lcos in H.
    spliter.
    ex_and H4 B.
    ex_and H5 A.
    ex_and H4 C.
    ex_and H1 P.
    unfold Q_Cong in H0.
    ex_and H0 X.
    ex_and H1 Y.
    assert(HH:= (H0 B A)).
    destruct HH.
    assert(HH:= (H0 P P)).
    destruct HH.
    apply H11 in H8.
    apply H9 in H5.
    assert(Cong B A P P).
      apply (cong_transitivity _ _ X Y); Cong.
    assert(A = B).
      eapply (cong_identity _ _ P).
      Cong.
    assert(HH:=anga_distincts a A B C H3 H7).
    spliter.
    contradiction.
Qed.

Lemma lcos_const_o : lp l a A B P, ¬ Col A B P ¬ Q_CongA_Null_Acute a Q_Cong l Q_Cong lp
  Q_CongA_Acute a l A B Lcos lp l a
   C, OS A B C P a A B C lp B C.
Proof.
    intros.
    assert(HH:= anga_const_o a A B P H H0 H3).
    ex_and HH C'.
    assert(A B C' B).
      apply (anga_distincts a); auto.
    spliter.
    assert(HH:= lcos_not_lg_null lp l a H5).
    assert (B C').
      intro.
      apply H9.
      auto.
    assert(HP:=lg_exists C' B).
    ex_and HP lc'.
    assert(HQ:=anga_not_lg_null a l lc' A B C' H1 H11 H3 H4 H12 H6).
    spliter.
    assert(HR:= ex_point_lg_out lp B C' H10 H2 HH).
    ex_and HR C.
     C.
    split.
      apply invert_one_side.
      apply one_side_symmetry.
      apply (out_out_one_side _ _ _ C').
        apply invert_one_side.
        apply one_side_symmetry.
        auto.
      apply l6_6.
      auto.
    split.
      eapply (anga_out_anga a A B C'); auto.
        apply out_trivial.
        auto.
      apply l6_6.
      auto.
    auto.
Qed.

Lemma flat_not_acute : A B C, Bet A B C ¬ Acute A B C.
Proof.
    intros.
    intro.
    unfold Acute in H0.
    ex_and H0 A'.
    ex_and H1 B'.
    ex_and H0 C'.
    unfold LtA in H1.
    spliter.
    unfold LeA in H1.
    ex_and H1 P'.
    unfold InAngle in H1.
    spliter.
    ex_and H6 X.
    apply conga_distinct in H3.
    spliter.
    assert(A C).
      intro.
      subst C.
      apply between_identity in H.
      contradiction.
    induction H7.
      subst X.
      apply H2.
      apply conga_line; auto.
    assert(CongA A B C A' B' X).
      apply (out_conga A B C A' B' P').
        auto.
        apply out_trivial; auto.
        apply out_trivial; auto.
        apply out_trivial; auto.
      apply l6_6.
      auto.
    apply H2.
    assert(Bet A' B' X).
      apply (bet_conga_bet A B C); auto.
    apply conga_line; auto.
    apply (between_exchange4 _ _ X); auto.
Qed.

Lemma acute_comp_not_acute : A B C D, Bet A B C Acute A B D ¬ Acute C B D.
Proof.
    intros.
    intro.
    induction(Col_dec A C D).
      induction H2.
        assert(Bet A B D).
          eBetween.
        assert(HH:= flat_not_acute A B D H3).
        contradiction.
      induction H2.
        assert(Bet A B D Bet A D B).
          apply (l5_3 A B D C).
            auto.
          Between.
        induction H3.
          assert(HH:= flat_not_acute A B D H3).
          contradiction.
        assert(Bet C B D).
          eBetween.
        assert(HH:= flat_not_acute C B D H4).
        contradiction.
      assert(Bet C B D).
        eBetween.
      assert(HH:= flat_not_acute C B D H3).
      contradiction.
    unfold Acute in ×.
    ex_and H0 A0.
    ex_and H3 B0.
    ex_and H0 C0.
    ex_and H1 A1.
    ex_and H4 B1.
    ex_and H1 C1.
    apply lta_diff in H3.
    apply lta_diff in H4.
    spliter.
    assert(HH:=l11_16 A0 B0 C0 A1 B1 C1 H0 H11 H12 H1 H7 H8).
    assert(LtA C B D A0 B0 C0).
      eapply(conga_preserves_lta C B D A1 B1 C1).
        apply conga_refl; auto.
        apply conga_sym.
        auto.
      auto.
    clear H4.
    assert(A C).
      intro.
      subst C.
      apply between_identity in H.
      contradiction.
    assert(Col A C B).
      apply bet_col in H.
      Col.
    assert(HP:= l10_15 A C B D H14 H2).
    ex_and HP P.
    assert(HP:= perp_col A C P B B H9 H15 H14).
    apply perp_left_comm in HP.
    apply perp_perp_in in HP.
    assert(Per A B P).
      apply perp_in_per.
      apply perp_in_comm.
      auto.
    assert(HR:= perp_not_eq_2 A C P B H15).
    assert(HQ:=l11_16 A B P A0 B0 C0 H17 H9 HR H0 H11 H12).
    assert(LtA A B D A B P).
      apply (conga_preserves_lta A B D A0 B0 C0); auto.
        apply conga_refl; auto.
      apply conga_sym.
      auto.
    assert(LtA C B D A B P).
      apply (conga_preserves_lta C B D A0 B0 C0); auto.
        apply conga_refl; auto.
      apply conga_sym.
      auto.
    clear HQ H13 H8 HH H3 H11 H12 H0 H1 H7.
    unfold LtA in ×.
    spliter.
    assert((LeA A B D A B P LeA C B P C B D)).
      apply (l11_36 A B D A B P C C); auto.
    destruct H8.
    assert(LeA C B P C B D).
      apply H8.
      auto.
    assert(CongA A B P C B P).
      apply l11_16; auto.
      apply perp_in_per.
      assert(Perp C B P B).
        apply(perp_col _ A).
          auto.
          apply perp_left_comm.
          auto.
        apply bet_col in H.
        Col.
      apply perp_in_comm.
      apply perp_perp_in.
      apply perp_left_comm.
      auto.
    assert(LeA A B P C B D).
      apply (l11_30 C B P C B D); auto.
        apply conga_sym.
        auto.
      apply conga_refl; auto.
    assert(HH:=lea_asym C B D A B P H0 H18).
    contradiction.
Qed.

Lemma lcos_per : A B C lp l a, Q_CongA_Acute a Q_Cong l Q_Cong lp
  Lcos lp l a l A C lp A B a B A C Per A B C.
Proof.
    intros.
    induction(eq_dec_points B C).
      subst C.
      apply l8_5.
    unfold Lcos in H2.
    spliter.
    ex_and H9 A0.
    ex_and H10 B0.
    ex_and H9 C0.
    assert(CongA B0 A0 C0 B A C).
      apply (anga_conga a); auto.
    assert(Cong A0 C0 A C).
      apply (lg_cong l); auto.
    assert(Cong A0 B0 A B).
      apply (lg_cong lp); auto.
    assert(HH:=l11_49 B0 A0 C0 B A C H13 H15 H14).
    spliter.
    assert(B0 C0).
      intro.
      subst C0.
      apply H6.
      apply (cong_identity _ _ B0).
      Cong.
    apply H17 in H18.
    spliter.
    eapply (l11_17 A0 B0 C0).
      apply l8_2.
      auto.
    auto.
Qed.

Lemma is_null_anga_dec : a, Q_CongA_Acute a Q_CongA_Null_Acute a ¬ Q_CongA_Null_Acute a.
Proof.
    intros a H.
    assert (H' := H).
    unfold Q_CongA_Acute in H.
    destruct H as [A [B [C [Hacute HConga]]]].
    elim (out_dec B A C); intro Hout.
      left.
      unfold Q_CongA_Null_Acute.
      split; auto.
      intros.
      apply (out_conga_out A B C); auto.
      apply HConga.
      assumption.
    right.
    unfold Q_CongA_Null_Acute.
    intro H.
    destruct H as [Hclear H]; clear Hclear.
    apply Hout.
    apply H.
    apply HConga.
    apply acute_distinct in Hacute.
    spliter.
    apply conga_refl; auto.
Qed.

Lemma lcos_lg : a lp l A B C, Lcos lp l a Perp A B B C a B A C l A C lp A B.
Proof.
    intros.
    assert(HH:=H).
    unfold Lcos in HH.
    spliter.
    ex_and H6 A'.
    ex_and H7 B'.
    ex_and H6 C'.
    assert(Cong A C A' C').
      apply (lg_cong l); auto.
    assert(CongA B A C B' A' C').
      apply (anga_conga a); auto.
    induction(is_null_anga_dec a).
      assert(HP := null_lcos_eql lp l a H H12).
      unfold Q_CongA_Null_Acute in H12.
      spliter.
      assert(HH:= (H13 B A C H1)).
      apply perp_comm in H0.
      apply perp_not_col in H0.
      apply False_ind.
      apply H0.
      apply out_col in HH.
      Col.
      apply conga_distinct in H11.
      spliter.
      assert(CongA A B C A' B' C').
        apply l11_16; auto.
          apply perp_in_per.
          apply perp_in_comm.
          apply perp_perp_in.
          apply perp_comm.
          auto.
          apply perp_not_eq_2 in H0.
          auto.
          apply l8_2.
          auto.
        intro.
        subst C'.
        apply H12.
        unfold Q_CongA_Null_Acute.
        split; auto.
        intros.
        assert(CongA A0 B0 C0 B' A' B').
          apply (anga_conga a); auto.
        apply (out_conga_out B' A' B') .
          apply out_trivial; auto.
        apply conga_sym.
        auto.
      assert(Cong C B C' B' Cong A B A' B' CongA B C A B' C' A').
        apply(l11_50_2 C A B C' A' B').
          apply perp_comm in H0.
          apply perp_not_col in H0.
          intro.
          apply H0.
          Col.
          auto.
          apply conga_comm.
          auto.
        Cong.
      spliter.
      apply (lg_cong_lg lp A' B');auto.
      Cong.
    assumption.
Qed.

Lemma l13_7 : a b l la lb lab lba, Lcos la l a Lcos lb l b
  Lcos lab la b Lcos lba lb a EqL lab lba.
Proof.
    intros.
    apply lcos_lg_anga in H.
    apply lcos_lg_anga in H0.
    apply lcos_lg_anga in H1.
    apply lcos_lg_anga in H2.
    spliter.
    clean_duplicated_hyps.
    induction (is_null_anga_dec a).
      assert(HH:=null_lcos_eql lba lb a H2 H3).
      assert(HP:=null_lcos_eql la l a H H3).
      assert(Lcos lab l b) by (rewrite HP;assumption).
      assert(HQ:= l13_6 b lb lab l H0 H5).
      rewrite <- HQ;assumption.
      induction (is_null_anga_dec b).
        assert(HH:=null_lcos_eql lab la b H1 H5).
        assert(HP:=null_lcos_eql lb l b H0 H5).
        assert(Lcos lba l a) by (rewrite HP;auto).
        assert(HQ:= l13_6 a la lba l H H6).
        rewrite HH in HQ;assumption.
        assert(HH:=lcos_const la l a H).
        ex_and HH C.
        ex_and H6 A.
        ex_and H8 B.
        assert(HH:= anga_distincts a C A B H14 H9).
        spliter.
        assert(¬Col A B C).
          intro.
          apply H3.
          assert(Col C A B).
            Col.
          assert(HH:= anga_col_null a C A B H14 H9 H18).
          spliter.
          auto.
        assert(HH:=l10_2_existence B A C).
        ex_and HH P.
        assert( ¬ Col B A P).
          eapply (osym_not_col _ _ C).
            apply l10_4.
            auto.
          intro.
          apply H17.
          Col.
        assert(l B A).
          apply lg_sym; auto.
        assert(HH:= lcos_const_o lb l b B A P H19 H5 H12 H10 H11 H20 H0).
        ex_and HH D.
        assert(TS B A P C).
          apply l10_14.
            intro.
            subst P.
            assert(Col C B A).
              apply(l10_8 B A C); auto.
            apply H19.
            Col.
            auto.
          auto.
        assert(TS B A D C).
          eapply (l9_8_2 _ _ P).
            auto.
          apply one_side_symmetry.
          auto.
        assert(Per A C B).
          apply (lcos_per _ _ _ la l a); auto.
          apply lg_sym; auto.
        assert(Per A D B).
          apply (lcos_per _ _ _ lb l b); auto.
          apply anga_sym; auto.
        assert(¬ Col C D A).
          intro.
          assert(Per B C D).
            apply(per_col B C A D); auto.
              apply l8_2.
              auto.
            Col.
          assert(Per B D C).
            apply(per_col B D A C); auto.
              unfold OS in H21.
              ex_and H21 T.
              unfold TS in H21.
              spliter.
              intro.
              subst D.
              apply H21.
              Col.
              apply l8_2.
              auto.
            Col.
          assert(C = D).
            apply (l8_7 B); auto.
          subst D.
          unfold TS in H25.
          spliter.
          ex_and H32 T.
          assert(C=T).
            apply between_identity.
            auto.
          subst T.
          contradiction.
        assert(HH:= l8_18_existence C D A H28).
        ex_and HH E.
        assert(CongA B A C D A E CongA B A D C A E Bet C E D).
          apply(l13_2 A B C D E).
            apply invert_two_sides.
            apply l9_2.
            auto.
            apply l8_2.
            auto.
            apply l8_2.
            auto.
            auto.
          apply perp_sym.
          auto.
        spliter.
        assert(a D A E).
          eapply (anga_conga_anga a B A C); auto.
          apply anga_sym; auto.
        assert(b C A E).
          eapply (anga_conga_anga b B A D); auto.
        assert(Perp C E A E).
          eapply (perp_col _ D) .
            intro.
            subst E.
            apply H5.
            unfold Q_CongA_Null_Acute.
            split; auto.
            intros.
            assert(CongA A0 B0 C0 C A C).
              apply (anga_conga b); auto.
            apply (out_conga_out C A C A0 B0 C0 ).
              apply out_trivial; auto.
            apply conga_sym.
            auto.
            auto.
          auto.
        assert(lab A E).
          apply (lcos_lg b lab la A E C H1).
            apply perp_sym in H36.
            apply perp_right_comm in H36.
            auto.
            apply anga_sym; auto.
          apply lg_sym; auto.
        assert(Perp D E A E).
          eapply (perp_col _ C) .
            intro.
            subst E.
            apply H3.
            unfold Q_CongA_Null_Acute.
            split; auto.
            intros.
            assert(CongA A0 B0 C0 D A D).
              apply (anga_conga a); auto.
            apply (out_conga_out D A D A0 B0 C0 ).
              apply out_trivial; auto.
              apply perp_not_eq_2 in H36.
              auto.
            apply conga_sym.
            auto.
            Perp.
          Col.
        assert(lba A E).
          apply (lcos_lg a lba lb A E D).
            auto.
            Perp.
            auto.
            apply anga_sym; auto.
          auto.
        apply ex_eql.
         A.
         E.
        split.
          unfold Len.
          split; auto.
        unfold Len.
        split; auto.
      assumption.
    assumption.
Qed.

Lemma out_acute : A B C, Out B A C Acute A B C.
Proof.
    intros.
    assert( A B C B).
      unfold Out in H.
      tauto.
    spliter.
    assert(HH:= not_col_exists A B H0).
    ex_and HH Q.
    assert( P : Tpoint, Perp A B P B OS A B Q P).
      apply(l10_15 A B B Q).
        Col.
      auto.
    ex_and H3 P.
    assert(Per P B A).
      apply perp_in_per.
      apply perp_left_comm in H3.
      apply perp_in_comm.
      apply perp_perp_in.
      Perp.
    unfold Acute.
     A.
     B.
     P.
    split.
      apply l8_2.
      auto.
    unfold LtA.
    split.
      unfold LeA.
       C.
      split.
        apply col_in_angle; auto.
        apply perp_not_eq_2 in H3.
        auto.
      apply conga_refl; auto.
    intro.
    apply out_conga_out in H6.
      apply perp_left_comm in H3.
      apply perp_not_col in H3.
      apply out_col in H6.
      contradiction.
    assumption.
Qed.

Lemma perp_acute : A B C P, Col A C P Perp_at P B P A C Acute A B P.
Proof.
    intros.
    assert(HH0:=H0).
    assert(HH:= l11_43 P A B).
    induction(Col_dec P A B).
      assert(Perp B A A C).
        eapply (perp_col _ P).
          intro.
          subst A.
          assert(Perp_at B B P C B).
            apply perp_perp_in.
            apply perp_in_perp_bis in H0.
            induction H0.
              apply perp_not_eq_1 in H0.
              tauto.
            Perp.
          assert(P=B).
            eapply(l8_14_3 B P B C); Perp.
          subst P.
          apply perp_in_perp_bis in H0.
          induction H0.
            apply perp_not_eq_1 in H0.
            tauto.
          apply perp_not_eq_1 in H0.
          tauto.
          apply perp_in_perp_bis in H0.
          induction H0.
            apply perp_not_eq_1 in H0.
            tauto.
          auto.
        Col.
      apply perp_comm in H2.
      apply perp_perp_in in H2.
      apply perp_in_comm in H2.
      apply perp_in_sym in H2.
      eapply (perp_in_col_perp_in _ _ _ _ P) in H2.
        assert( A = P).
          eapply(l8_14_3 A C B P); Perp.
        subst P.
        apply out_acute.
        apply perp_in_perp_bis in H2.
        induction H2.
          apply out_trivial.
          apply perp_not_eq_2 in H2.
          auto.
        apply perp_not_eq_1 in H2.
        tauto.
        apply perp_in_perp_bis in H0.
        induction H0; apply perp_not_eq_1 in H0; tauto.
      Col.
    apply acute_sym.
    apply l11_43.
      auto.
    left.
    assert(A P).
      intro.
      subst P.
      apply H1.
      Col.
    eapply (perp_in_col_perp_in _ _ _ _ P) in H0; auto.
    apply perp_in_per.
    Perp.
Qed.

Lemma null_lcos : l a,Q_Cong l ¬ Q_Cong_Null l Q_CongA_Null_Acute a Lcos l l a.
Proof.
    intros.
    unfold Q_CongA_Null_Acute in H1.
    spliter.
    assert(HH:=ex_points_anga a H1).
    ex_and HH A.
    ex_and H3 B.
    ex_and H4 C.
    assert(HH:=H2 A B C H3).
    unfold Lcos.
    repeat split; auto.
    assert(B A).
      unfold Out in HH.
      spliter.
      auto.
    lg_instance l A' B'.
    assert(HP:=ex_point_lg_out l B A H4 H H0).
    ex_and HP P.
     B.
     P.
     P.
    repeat split; auto.
      apply l8_2.
      apply l8_5.
    apply (anga_out_anga _ A _ C); auto.
      apply l6_6.
      auto.
    apply (out2_out_2 _ _ _ A).
      apply l6_6.
      auto.
    auto.
Qed.

Lemma lcos_exists : l a, Q_CongA_Acute a Q_Cong l ¬ Q_Cong_Null l lp, Lcos lp l a.
Proof.
    intros.
    lg_instance l A B.
    induction(is_null_anga_dec a).
       l.
      apply null_lcos; auto.
      anga_instance1 a A B C.
        assert(¬ Col B C A).
          intro.
          assert(Out B A C Q_CongA_Null_Acute a).
            apply(anga_col_null a A B C H H4).
            Col.
          apply H3.
          tauto.
        assert(HH:= l8_18_existence B C A H5).
        ex_and HH P.
        assert(HH:=lg_exists B P).
        ex_and HH lp.
         lp.
        assert(Acute A B C).
          unfold Q_CongA_Acute in H.
          ex_and H A'.
          ex_and H10 B'.
          ex_and H C'.
          assert(HH:=H10 A B C).
          destruct HH.
          assert(HP:= H12 H4).
          apply (acute_lea_acute _ _ _ A' B' C'); auto.
          unfold LeA.
           C'.
          split.
            apply in_angle_trivial_2.
              apply conga_distinct in HP.
              tauto.
            apply conga_distinct in HP.
            tauto.
          apply conga_sym.
          auto.
        unfold Lcos.
        repeat split; auto.
         B.
         P.
         A.
        repeat split; auto.
          apply perp_in_per.
          apply perp_in_comm.
          apply perp_perp_in.
          apply perp_sym.
          apply (perp_col _ C).
            intro.
            subst P.
            assert(Per A B C).
              apply perp_in_per.
              apply perp_in_comm.
              apply perp_perp_in.
              Perp.
            apply acute_not_per in H10.
            contradiction.
            Perp.
          Col.
          apply (lg_sym l); auto.
        assert(HH:=H10).
        unfold Acute in HH.
        apply(anga_sym a); auto.
        apply(anga_out_anga a A B C A P); auto.
          apply out_trivial.
          intro.
          subst B.
          apply H5.
          Col.
        eapply (perp_acute_out _ _ A).
          apply acute_sym.
          auto.
          Perp.
        Col.
      intro.
      apply H1.
      unfold Q_Cong_Null.
      split; auto.
      subst B.
       A.
      auto.
    assumption.
Qed.

Lemma lcos_uniqueness : l a l1 l2, Lcos l1 l a Lcos l2 l a EqL l1 l2.
Proof.
intros.
unfold Lcos in ×.
spliter.
ex_and H6 A1.
ex_and H7 B1.
ex_and H6 C1.
ex_and H3 A2.
ex_and H10 B2.
ex_and H3 C2.

assert(Cong A1 C1 A2 C2).
apply (lg_cong l); auto.

assert(CongA B1 A1 C1 B2 A2 C2).
apply (anga_conga a); auto.

induction(eq_dec_points C1 B1).
subst C1.

assert(EqL l l1).
apply ex_eqL; auto.
A1.
B1.
split; auto.

assert(Out A2 B2 C2).
apply (out_conga_out B1 A1 B1).
apply out_trivial.
intro.
subst B1.
apply conga_distinct in H14.
tauto.
auto.

assert(C2 = B2 A2 = B2).
apply(l8_9 C2 B2 A2).
auto.
apply out_col in H16.
Col.
induction H17.
subst C2.

assert(EqL l l2).
apply ex_eqL; auto.
A2.
B2.
split; auto.
transitivity l; auto.
symmetry; auto.

subst B2.
apply conga_distinct in H14.
tauto.

apply conga_distinct in H14.
spliter.
assert(CongA C1 B1 A1 C2 B2 A2).
apply l11_16; auto.
intro.
subst C2.

assert(Out A1 B1 C1).
apply (out_conga_out B2 A2 B2).
apply out_trivial; auto.
apply conga_sym.
auto.
assert(C1 = B1 A1 = B1).
apply(l8_9 C1 B1 A1 ); auto.
apply out_col in H20.
Col.
induction H21.
subst C1.
tauto.
subst B1.
tauto.

assert( Cong C1 B1 C2 B2 Cong A1 B1 A2 B2 CongA B1 C1 A1 B2 C2 A2).
apply(l11_50_2 C1 A1 B1 C2 A2 B2).
intro.
assert(C1 = B1 A1 = B1).
apply(l8_9 C1 B1 A1 ); auto.
Col.
induction H22.
contradiction.
subst B1.
tauto.
apply conga_comm.
auto.
apply conga_comm.
auto.
Cong.
spliter.

apply ex_eqL; auto.
A1.
B1.
split; auto.
apply (lg_cong_lg l2 A2 B2); auto.
Cong.
Qed.

Lemma lcos_eqa_lcos : lp l a b, Lcos lp l a EqA a b Lcos lp l b.
Proof.
    intros.
    assert(HH:=lcos_lg_anga l lp a H).
    spliter.
    clear H1.
    assert(HH:= H0).
    unfold EqA in HH.
    assert (Q_CongA a) by (apply anga_is_ang;auto).
    assert (Q_CongA b) by (apply eqA_preserves_ang with a;auto).
    assert (Q_CongA_Acute b).
      apply (eqA_preserves_anga a b); auto.
    unfold Lcos in ×.
    spliter.
    repeat split; auto.
    ex_and H9 A.
    ex_and H10 B.
    ex_and H9 C.
     A.
     B.
     C.
    repeat split; auto.
    apply HH;auto.
Qed.

Definition Eq_Lcos la a lb b := lp, Lcos lp la a Lcos lp lb b.

Lemma lcos_eq_refl : la a, Q_Cong la ¬ Q_Cong_Null la Q_CongA_Acute a Eq_Lcos la a la a.
Proof.
    intros.
    unfold Eq_Lcos.
    assert(HH:=lcos_exists la a H1 H H0).
    ex_and HH lp.
     lp.
    split; auto.
Qed.

Lemma lcos_eq_sym : la a lb b, Eq_Lcos la a lb b Eq_Lcos lb b la a.
Proof.
    intros.
    unfold Eq_Lcos in ×.
    ex_and H lp.
     lp.
    split; auto.
Qed.

Lemma lcos_eq_trans : la a lb b lc c, Eq_Lcos la a lb b Eq_Lcos lb b lc c Eq_Lcos la a lc c.
Proof.
    intros.
    unfold Eq_Lcos in ×.
    ex_and H lab.
    ex_and H0 lbc.
    assert(HH:= l13_6 b lab lbc lb H1 H0).
    assert(Lcos lbc la a).
      rewrite <- HH.
      apply lcos_lg_anga in H.
      tauto.
     lbc.
    split; auto.
Qed.

Definition lcos2 lp l a b := la, Lcos la l a Lcos lp la b.

Lemma lcos2_comm : lp l a b, lcos2 lp l a b lcos2 lp l b a.
Proof.
    intros.
    unfold lcos2 in ×.
    ex_and H la.
    apply lcos_lg_anga in H.
    apply lcos_lg_anga in H0.
    spliter.
    assert( lb, Lcos lb l b).
      apply(lcos_exists l b); auto.
      assert(HH:= lcos_lg_not_null la l a H).
      tauto.
    ex_and H7 lb.
    apply lcos_lg_anga in H8.
    spliter.
     lb.
    split.
      auto.
    assert( lp', Lcos lp' lb a).
      apply(lcos_exists lb a); auto.
      assert(HH:= lcos_lg_not_null lb l b H7).
      tauto.
    ex_and H11 lp'.
    assert(EqL lp lp').
      apply(l13_7 a b l la lb lp lp'); auto.
    apply lcos_lg_anga in H12.
    rewrite H11. tauto.
Qed.

Lemma lcos2_exists : l a b, Q_Cong l ¬ Q_Cong_Null l Q_CongA_Acute a Q_CongA_Acute b
  lp, lcos2 lp l a b.
Proof.
    intros.
    assert(HH:= lcos_exists l a H1 H H0).
    ex_and HH la.
    apply lcos_lg_anga in H3.
    spliter.
    assert(¬ Q_Cong_Null la ¬ Q_Cong_Null l).
      apply (lcos_lg_not_null _ _ a).
      auto.
    spliter.
    clear H8.
    assert(HH:= lcos_exists la b H2 H5 H7).
    ex_and HH lab.
     lab.
    unfold lcos2.
     la.
    split; auto.
Qed.

Lemma lcos2_exists' : l a b, Q_Cong l ¬ Q_Cong_Null l Q_CongA_Acute a Q_CongA_Acute b
  la, lab, Lcos la l a Lcos lab la b.
Proof.
    intros.
    assert(HH:=lcos_exists l a H1 H H0).
    ex_and HH la.
     la.
    apply lcos_lg_anga in H3.
    spliter.
    assert(HP:=lcos_not_lg_null la l a H3).
    assert(HH:=lcos_exists la b H2 H5 HP).
    ex_and HH lab.
     lab.
    split; auto.
Qed.

Definition Eq_Lcos2 l1 a b l2 c d := lp, lcos2 lp l1 a b lcos2 lp l2 c d.

Lemma lcos2_eq_refl : l a b, Q_Cong l ¬ Q_Cong_Null l Q_CongA_Acute a Q_CongA_Acute b Eq_Lcos2 l a b l a b.
Proof.
    intros.
    assert(HH:= lcos2_exists l a b H H0 H1 H2).
    ex_and HH lab.
    unfold Eq_Lcos2.
     lab.
    split; auto.
Qed.

Lemma lcos2_eq_sym : l1 a b l2 c d, Eq_Lcos2 l1 a b l2 c d Eq_Lcos2 l2 c d l1 a b.
Proof.
    intros.
    unfold Eq_Lcos2 in ×.
    ex_and H lp.
     lp.
    auto.
Qed.

Lemma lcos2_uniqueness: l l1 l2 a b, lcos2 l1 l a b lcos2 l2 l a b EqL l1 l2.
Proof.
    intros.
    unfold lcos2 in ×.
    ex_and H la.
    ex_and H0 lb.
    assert(EqL la lb).
      apply (l13_6 a _ _ l); auto.
    apply lcos_lg_anga in H2.
    apply lcos_lg_anga in H1.
    spliter.
    assert(Lcos l2 la b).
      rewrite H3;auto.
    apply (l13_6 b _ _ la); auto.
Qed.

Lemma lcos2_eql_lcos2 : lla llb la lb a b, lcos2 la lla a b EqL lla llb EqL la lb lcos2 lb llb a b.
Proof.
    intros.
    unfold lcos2 in ×.
    ex_and H l.
     l.
    apply lcos_lg_anga in H.
    apply lcos_lg_anga in H2.
    spliter.
    split.
    rewrite <- H0;auto.
    rewrite <- H1;auto.
Qed.

Lemma lcos2_lg_anga : lp l a b, lcos2 lp l a b lcos2 lp l a b Q_Cong lp Q_Cong l Q_CongA_Acute a Q_CongA_Acute b.
Proof.
    intros.
    split; auto.
    unfold lcos2 in H.
    ex_and H ll.
    apply lcos_lg_anga in H.
    apply lcos_lg_anga in H0.
    spliter.
    split; auto.
Qed.

Lemma lcos2_eq_trans : l1 a b l2 c d l3 e f, Eq_Lcos2 l1 a b l2 c d Eq_Lcos2 l2 c d l3 e f
                                    Eq_Lcos2 l1 a b l3 e f.
Proof.
    intros.
    unfold Eq_Lcos2 in ×.
    ex_and H lp.
    ex_and H0 lq.
     lp.
    split; auto.
    assert(EqL lp lq).
      eapply (lcos2_uniqueness l2 _ _ c d); auto.
    apply lcos2_lg_anga in H2.
    apply lcos2_lg_anga in H1.
    spliter.
    eapply (lcos2_eql_lcos2 l3 _ lq); auto.
      reflexivity.
    symmetry; auto.
Qed.

Lemma lcos_eq_lcos2_eq : la lb a b c, Q_CongA_Acute c Eq_Lcos la a lb b Eq_Lcos2 la a c lb b c.
Proof.
    intros.
    assert(HH0:=H0).
    unfold Eq_Lcos in HH0.
    ex_and HH0 lp.
    apply lcos_lg_anga in H1.
    apply lcos_lg_anga in H2.
    spliter.
    clear H7.
    assert(¬ Q_Cong_Null lp ¬ Q_Cong_Null la).
      apply (lcos_lg_not_null _ _ a).
      auto.
    spliter.
    unfold Eq_Lcos2.
    assert(HH:= lcos_exists lp c H H4 H7).
    ex_and HH lq.
     lq.
    split.
      unfold lcos2.
       lp.
      split; auto.
    unfold lcos2.
     lp.
    split; auto.
Qed.

Lemma lcos2_lg_not_null: lp l a b, lcos2 lp l a b ¬ Q_Cong_Null l ¬ Q_Cong_Null lp.
Proof.
    intros.
    unfold lcos2 in H.
    ex_and H la.
    apply lcos_lg_not_null in H.
    apply lcos_lg_not_null in H0.
    spliter.
    split; auto.
Qed.

Definition Lcos3 lp l a b c := la, lab, Lcos la l a Lcos lab la b Lcos lp lab c.

Lemma lcos3_lcos_1_2 : lp l a b c, Lcos3 lp l a b c la, Lcos la l a lcos2 lp la b c.
Proof.
    intros.
    split.
      intro.
      unfold Lcos3 in H.
      ex_and H la.
      ex_and H0 lab.
       la.
      split; auto.
      unfold lcos2.
       lab.
      split; auto.
    intro.
    ex_and H la.
    unfold lcos2 in H0.
    ex_and H0 lab.
    unfold Lcos3.
     la.
     lab.
    apply lcos_lg_anga in H0.
    apply lcos_lg_anga in H1.
    spliter.
    split; auto.
Qed.

Lemma lcos3_lcos_2_1 : lp l a b c, Lcos3 lp l a b c lab, lcos2 lab l a b Lcos lp lab c.
Proof.
    intros.
    split.
      intro.
      unfold Lcos3 in H.
      ex_and H la.
      ex_and H0 lab.
       lab.
      split.
        unfold lcos2.
         la.
        split; assumption.
      assumption.
    intro.
    ex_and H lab.
    unfold Lcos3.
    unfold lcos2 in H.
    ex_and H la.
     la.
     lab.
    split; auto.
Qed.

Lemma lcos3_permut3 : lp l a b c, Lcos3 lp l a b c Lcos3 lp l b a c.
Proof.
    intros.
    assert(HH:= lcos3_lcos_2_1 lp l a b c).
    destruct HH.
    assert( lab : Tpoint Tpoint Prop, lcos2 lab l a b Lcos lp lab c).
      apply lcos3_lcos_2_1; auto.
    ex_and H2 lab.
    apply lcos2_comm in H2.
    apply lcos3_lcos_2_1.
     lab.
    split; auto.
Qed.

Lemma lcos3_permut1 : lp l a b c, Lcos3 lp l a b c Lcos3 lp l a c b.
Proof.
    intros.
    assert(HH:= lcos3_lcos_1_2 lp l a b c).
    destruct HH.
    assert( la : Tpoint Tpoint Prop, Lcos la l a lcos2 lp la b c).
      apply lcos3_lcos_1_2; auto.
    ex_and H2 la.
    apply lcos2_comm in H3.
    apply lcos3_lcos_1_2.
     la.
    split; auto.
Qed.

Lemma lcos3_permut2 : lp l a b c, Lcos3 lp l a b c Lcos3 lp l c b a.
Proof.
    intros.
    apply lcos3_permut3.
    apply lcos3_permut1.
    apply lcos3_permut3.
    auto.
Qed.

Lemma lcos3_exists : l a b c, Q_Cong l ¬ Q_Cong_Null l Q_CongA_Acute a Q_CongA_Acute b Q_CongA_Acute c
  lp, Lcos3 lp l a b c.
Proof.
    intros.
    assert(HH:= lcos_exists l a H1 H H0).
    ex_and HH la.
    apply lcos_lg_anga in H4.
    spliter.
    assert(¬ Q_Cong_Null la ¬ Q_Cong_Null l).
      apply (lcos_lg_not_null _ _ a).
      auto.
    spliter.
    clear H9.
    clear H7.
    assert(HH:= lcos_exists la b H2 H6 H8).
    ex_and HH lab.
    apply lcos_lg_anga in H7.
    spliter.
    assert(¬ Q_Cong_Null lab ¬ Q_Cong_Null la).
      apply (lcos_lg_not_null _ _ b).
      auto.
    spliter.
    assert(HH:= lcos_exists lab c H3 H10 H12).
    ex_and HH lp.
     lp.
    unfold Lcos3.
     la.
     lab.
    split;auto.
Qed.


Definition Eq_Lcos3 l1 a b c l2 d e f := lp, Lcos3 lp l1 a b c Lcos3 lp l2 d e f.

Lemma lcos3_eq_refl : l a b c, Q_Cong l ¬ Q_Cong_Null l Q_CongA_Acute a Q_CongA_Acute b Q_CongA_Acute c Eq_Lcos3 l a b c l a b c.
Proof.
    intros.
    assert(HH:= lcos3_exists l a b c H H0 H1 H2 H3).
    ex_and HH lp.
    unfold Eq_Lcos3.
     lp.
    split; auto.
Qed.

Lemma lcos3_eq_sym : l1 a b c l2 d e f, Eq_Lcos3 l1 a b c l2 d e f Eq_Lcos3 l2 d e f l1 a b c.
Proof.
    intros.
    unfold Eq_Lcos3 in ×.
    ex_and H lp.
     lp.
    auto.
Qed.

Lemma lcos3_uniqueness: l l1 l2 a b c, Lcos3 l1 l a b c Lcos3 l2 l a b c EqL l1 l2.
Proof.
    intros.
    unfold Lcos3 in ×.
    ex_and H la.
    ex_and H1 lab.
    ex_and H0 la'.
    ex_and H3 lab'.
    assert(EqL la la').
      apply (l13_6 a _ _ l); auto.
    apply lcos_lg_anga in H2.
    apply lcos_lg_anga in H3.
    apply lcos_lg_anga in H.
    apply lcos_lg_anga in H4.
    spliter.
    assert(Lcos lab' la b).
      rewrite H5;auto.
    assert(EqL lab lab') by
      (apply (l13_6 b _ _ la); auto).
    assert(Lcos l2 lab c).
      rewrite H19. auto.
    apply (l13_6 c _ _ lab); auto.
Qed.

Lemma lcos3_eql_lcos3 : lla llb la lb a b c, Lcos3 la lla a b c EqL lla llb EqL la lb Lcos3 lb llb a b c.
Proof.
    intros.
    unfold Lcos3 in ×.
    ex_and H lpa.
     lpa.
    ex_and H2 lpab.
     lpab.
    apply lcos_lg_anga in H.
    apply lcos_lg_anga in H2.
    apply lcos_lg_anga in H3.
    spliter.
    split.
    rewrite <- H0;auto.
    split.
      auto.
    rewrite <- H1;auto.
Qed.

Lemma lcos3_lg_anga : lp l a b c, Lcos3 lp l a b c Lcos3 lp l a b c Q_Cong lp Q_Cong l Q_CongA_Acute a Q_CongA_Acute b Q_CongA_Acute c.
Proof.
    intros.
    split; auto.
    unfold Lcos3 in H.
    ex_and H la.
    ex_and H0 lab.
    apply lcos_lg_anga in H.
    apply lcos_lg_anga in H0.
    apply lcos_lg_anga in H1.
    spliter.
    split; auto.
Qed.

Lemma lcos3_lg_not_null: lp l a b c, Lcos3 lp l a b c ¬ Q_Cong_Null l ¬ Q_Cong_Null lp.
Proof.
    intros.
    unfold Lcos3 in H.
    ex_and H la.
    ex_and H0 lab.
    apply lcos_lg_not_null in H.
    apply lcos_lg_not_null in H1.
    spliter.
    split; auto.
Qed.

Lemma lcos3_eq_trans : l1 a b c l2 d e f l3 g h i,
 Eq_Lcos3 l1 a b c l2 d e f Eq_Lcos3 l2 d e f l3 g h i Eq_Lcos3 l1 a b c l3 g h i.
Proof.
    intros.
    unfold Eq_Lcos3 in ×.
    ex_and H lp.
    ex_and H0 lq.
     lp.
    split; auto.
    assert(EqL lp lq).
      eapply (lcos3_uniqueness l2 _ _ d e f); auto.
    apply lcos3_lg_anga in H2.
    apply lcos3_lg_anga in H1.
    spliter.
    eapply (lcos3_eql_lcos3 l3 _ lq); auto.
      reflexivity.
    symmetry; auto.
Qed.

Lemma lcos_eq_lcos3_eq : la lb a b c d, Q_CongA_Acute c Q_CongA_Acute d Eq_Lcos la a lb b Eq_Lcos3 la a c d lb b c d.
Proof.
    intros.
    assert(HH1:=H1).
    unfold Eq_Lcos in HH1.
    ex_and HH1 lp.
    apply lcos_lg_anga in H2.
    apply lcos_lg_anga in H3.
    spliter.
    assert(¬ Q_Cong_Null lp ¬ Q_Cong_Null la).
      apply (lcos_lg_not_null _ _ a).
      auto.
    spliter.
    assert(HH:= lcos_exists lp c H H5 H10).
    ex_and HH lq.
    apply lcos_lg_anga in H12.
    spliter.
    assert(¬ Q_Cong_Null lq ¬ Q_Cong_Null lp).
      apply (lcos_lg_not_null _ _ c); auto.
    spliter.
    assert(HH:= lcos_exists lq d H0 H14 H16).
    ex_and HH lm.
    unfold Eq_Lcos3.
     lm.
    split; unfold Lcos3.
       lp.
       lq.
      split; auto.
     lp.
     lq.
    split; auto.
Qed.

Lemma lcos2_eq_lcos3_eq : la lb a b c d e, Q_CongA_Acute e Eq_Lcos2 la a b lb c d Eq_Lcos3 la a b e lb c d e.
Proof.
    intros.
    assert(HH0:=H0).
    unfold Eq_Lcos2 in HH0.
    ex_and HH0 lp.
    apply lcos2_lg_anga in H1.
    apply lcos2_lg_anga in H2.
    spliter.
    assert(¬ Q_Cong_Null la ¬ Q_Cong_Null lp).
      eapply (lcos2_lg_not_null _ _ a b).
      auto.
    spliter.
    assert(HH:= lcos_exists lp e H H3 H12).
    ex_and HH lq.
    apply lcos_lg_anga in H13.
    spliter.
    assert(¬ Q_Cong_Null lq ¬ Q_Cong_Null lp).
      apply (lcos_lg_not_null _ _ e); auto.
    spliter.
    unfold Eq_Lcos3.
     lq.
    split; apply lcos3_lcos_2_1; lp; split; auto.
Qed.

End Cosinus2.