proposition: Lemma l11_13 : forall A B C D E F A' D', CongA A B C D E F -> Bet A B A' -> A'<> B -> Bet D E D' -> D'<> E -> CongA A' B C D' E F.
proof: Proof. intros. unfold CongA in H. spliter. ex_and H7 A''. ex_and H8 C''. ex_and H7 D''. ex_and H8 F''. prolong B A' A0 E D'. prolong E D' D0 B A'. unfold CongA. repeat split; try assumption. exists A0. exists C''. exists D0. exists F''. repeat split; try assumption. apply (five_segment_with_def A'' B A0 C'' D'' E D0 F''). unfold OFSC. repeat split. eapply outer_transitivity_between2. apply between_symmetry. apply H7. eapply outer_transitivity_between. apply H0. assumption. auto. assumption. eapply outer_transitivity_between2. apply between_symmetry. apply H11. eapply outer_transitivity_between. apply H2. assumption. auto. assumption. apply cong_left_commutativity. eapply l2_11. apply H7. apply between_symmetry. apply H11. Cong. Cong. apply cong_right_commutativity. eapply l2_11. apply H16. apply between_symmetry. apply H18. apply cong_symmetry. Cong. Cong. assumption. apply cong_right_commutativity. apply l2_11 with C F; Cong; Between. assert_diffs;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2