proposition: Lemma conga2_cop2__col : forall A B C P P', ~ Out B A C -> CongA P B A P B C -> CongA P' B A P' B C -> Coplanar A B P P' -> Coplanar B C P P' -> Col B P P'.
proof: Proof. intros A B C P P' HNOut HP HP' HCopA HCopC. apply conga_distinct in HP; apply conga_distinct in HP'; spliter; clean. destruct (l6_11_existence B B A C) as [C' [HC'1 HC'2]]; auto. destruct (l11_49 P B A P B C'); Cong. apply l11_10 with P A P C; try apply out_trivial; auto. destruct (l11_49 P' B A P' B C'); Cong. apply l11_10 with P' A P' C; try apply out_trivial; auto. apply cong3_cop2__col with A C'; Cong. Cop. apply coplanar_perm_12, col_cop__cop with C; Col; Cop. intro; subst; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2