proposition: Lemma col_conga__conga : forall A B C P P', CongA P B A P B C -> Col B P P' -> B <> P' -> CongA P' B A P' B C.
proof: Proof. intros A B C P P' HConga HCol HBP'. destruct (bet_dec P B P') as [HBet|HNBet]. apply l11_13 with P P; auto. apply not_bet_out in HNBet; Col. apply l6_6 in HNBet. apply conga_distinct in HConga; spliter. apply l11_10 with P A P C; try (apply out_trivial); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2