proposition: Lemma lcos_per_anga : forall O A P la lp a, Lcos lp la a -> la O A -> lp O P -> Per A P O -> a A O P.
proof: Proof. intros. assert(HH:= H). unfold Lcos in HH. spliter. ex_and H6 O'. ex_and H7 P'. ex_and H6 A'. assert(Cong O A O' A'). apply (lg_cong la); auto. assert(Cong O P O' P'). apply (lg_cong lp); auto. assert(HH:= lcos_lg_not_null lp la a H). spliter. induction(eq_dec_points A P). subst A. assert(Cong O' A' O' P'). apply (cong_transitivity _ _ O P); Cong. assert(A' = P'). induction(col_dec A' P' O'). assert(A' = P' \/ O' = P'). apply l8_9; auto. induction H16. auto. subst P'. eapply (cong_identity _ O' O'); Cong. assert(Lt P' A' A' O' /\ Lt P' O' A' O'). assert_diffs; apply(l11_46 A' P' O'); auto. spliter. unfold Lt in H17. spliter. apply False_ind. apply H18. Cong. subst A'. assert(Q_CongA_Null_Acute a). apply(out_null_anga a P' O' P'); auto. apply out_trivial. intro. subst P'. apply H12. unfold Q_Cong_Null. split. auto. exists O'. auto. apply(is_null_all a P O). intro. subst P. apply H12. unfold Q_Cong_Null. split. auto. exists O. auto. auto. assert(O <> P). intro. subst P. apply H12. split. auto. exists O. auto. induction(col_dec A P O). assert (HH:=anga_distincts a P' O' A' H5 H9). spliter. assert(A' <> P'). intro. subst A'. assert(A = P \/ O = P). apply l8_9; auto. induction H19. auto. contradiction. assert(~ Col A P O). apply(per_not_col A P O); auto. contradiction. assert (HH:=anga_distincts a P' O' A' H5 H9). spliter. assert(A' <> P'). intro. subst A'. assert(Cong O P O A). apply (cong_transitivity _ _ O' P'); Cong. assert(Lt P A A O /\ Lt P O A O). assert_diffs; apply(l11_46 A P O); auto. spliter. unfold Lt in H21. spliter. apply H22. Cong. assert(CongA A P O A' P' O'). apply l11_16; auto. assert(Cong P A P' A' /\ CongA P A O P' A' O' /\ CongA P O A P' O' A'). assert(Lt P A A O /\ Lt P O A O). assert_diffs; apply(l11_46 A P O); auto. spliter. unfold Lt in H22. spliter. apply(l11_52 A P O A' P' O' ); Cong. spliter. apply conga_comm in H23. apply (anga_conga_anga a A' O' P'); auto. apply (anga_sym a); auto. apply conga_sym. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project