proposition: Lemma l11_22 : forall A B C P A' B' C' P', ((TS B P A C /\ TS B' P' A' C')\/ (OS B P A C /\ OS B' P' A' C')) /\ CongA A B P A' B' P' /\ CongA P B C P' B' C' -> CongA A B C A' B' C'.
proof: Proof. intros. spliter. induction H. apply (l11_22a _ _ _ P _ _ _ P');tauto. apply (l11_22b _ _ _ P _ _ _ P');tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2