proposition: Lemma lcos_per : forall 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: 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.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms