proposition: Lemma acute_comp_not_acute : forall A B C D, Bet A B C -> Acute A B D -> ~ Acute C B D.
proof: 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. assert (Hd := H3). assert (Hd' := H4). apply lta_distincts in Hd. apply lta_distincts in Hd'. spliter. assert(HH:=l11_16 A0 B0 C0 A1 B1 C1 H0 H12 H13 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 H16 H2). ex_and HP P. assert(HP:= perp_col A C P B B H10 H17 H16). 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 H17). assert(HQ:=l11_16 A B P A0 B0 C0 H19 H10 HR H0 H12 H13). 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 H15 HH H3 H0 H1. 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 H20. assert(LeA C B P C B D). apply H20. 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 H24). contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms