proposition: Lemma l11_3 : forall A B C D E F, CongA A B C D E F -> exists A', exists C', exists D', exists F', Out B A' A /\ Out B C C' /\ Out E D' D /\ Out E F F' /\ Cong_3 A' B C' D' E F'.
proof: Proof. intros. unfold CongA in H. spliter. ex_and H3 A'. ex_and H4 C'. ex_and H3 D'. ex_and H4 F'. exists A'. exists C'. exists D'. exists F'. assert_diffs. repeat split; auto; apply cong_left_commutativity. apply l2_11 with A D; Cong; Between. apply l2_11 with C F; Cong; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2