proposition: Lemma conga_cop_out_reflectl__out : forall A B C P T T', ~ Out B A C -> Coplanar A B C P -> CongA P B A P B C -> Out B A T -> ReflectL T T' B P -> Out B C T'.
proof: Proof. intros A B C P T T' HNOut HCop HConga HOut HRefl. apply conga_distinct in HConga; spliter; clean. assert_diffs. assert (HConga1 : CongA P B T P B T') by (apply reflectl__conga; auto; apply is_image_spec_rev, HRefl). apply is_image_is_image_spec in HRefl; auto. apply conga_distinct in HConga1; spliter; clean. apply (conga_os__out P). - apply conga_trans with P B A. apply conga_sym; assumption. apply l11_10 with P T P T'; try (apply out_trivial); auto. - exists A; split; apply l9_2. destruct (conga_cop__or_out_ts P B A C); Cop; contradiction. apply out_two_sides_two_sides with T B; Col. apply invert_two_sides, l10_14; auto. intro; subst T'. apply HNOut. assert (Col T B P) by (apply l10_8, HRefl). assert (Col P B A) by ColR. assert (Col P B C) by (apply (col_conga_col P B A); assumption). apply not_bet_out; try ColR. intro HBet. apply (per_not_col P B A); auto. apply l11_18_2 with C; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2