proposition: Lemma col_conga_cop_reflectl__col : forall A B C P T T', ~ Out B A C -> Coplanar A B C P -> CongA P B A P B C -> Col B A T -> ReflectL T T' B P -> Col B C T'.
proof: Proof. intros A B C P T T' HNOut HCop HConga HCol HRefl. destruct (eq_dec_points B T). subst; assert (T = T'); subst; Col. apply (l10_6_uniqueness_spec T P T); trivial; apply col__refl; Col. destruct (out_dec B A T). apply out_col, conga_cop_out_reflectl__out with A P T; assumption. destruct (segment_construction A B A B) as [A' [HA'1 HA'2]]. destruct (segment_construction C B C B) as [C' [HC'1 HC'2]]. assert (Out B C' T'); try ColR. apply conga_distinct in HConga; spliter; assert_diffs. apply conga_cop_out_reflectl__out with A' P T; trivial. - intro; apply HNOut. apply l6_2 with A'; auto. apply between_symmetry, l6_2 with C'; try (apply l6_6); Between. - destruct (col_dec A B C). exists C'; left; split; ColR. apply coplanar_pseudo_trans with A B C; Cop. - apply conga_comm, l11_13 with A C; auto; apply conga_comm; assumption. - apply l6_2 with A; try (apply between_symmetry); auto. apply not_out_bet; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2