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