proposition: Lemma perp_acute : forall A B C P, Col A C P -> Perp_at P B P A C -> Acute A B P.
proof: 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. assert_diffs. 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.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms