proposition: Lemma lcos_lcos_cop__col : forall la lb lp a b O A B P, Lcos lp la a -> Lcos lp lb b -> la O A -> lb O B -> lp O P -> a A O P -> b B O P -> Coplanar O A B P -> Col A B P.
proof: Proof. intros. apply lcos_lg_anga in H. apply lcos_lg_anga in H0. spliter. assert(Per O P A). apply (lcos_per O P A lp la a); auto. apply anga_sym; auto. assert(Per O P B). apply (lcos_per O P B lp lb b); auto. apply anga_sym; auto. apply cop_per2__col with O; Perp. intro. subst P. assert(HH:=lcos_lg_not_null lp la a H). spliter. apply H15. unfold Q_Cong_Null. split; auto. exists O. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project