proposition: Lemma l11_21_a : forall A B C A' B' C', Out B A C -> CongA A B C A' B' C' -> Out B' A' C'.
proof: Proof. intros. unfold CongA in H0. spliter. ex_and H4 A0. ex_and H5 C0. ex_and H4 A1. ex_and H5 C1. assert (Out B A0 C0). unfold Out. repeat split. intro. subst A0. apply between_identity in H4. subst A. absurde. intro. subst C0. apply between_identity in H6. subst C. absurde. unfold Out in H. spliter. induction H14. apply l5_1 with A; auto. eapply between_exchange4. apply H14. assumption. apply l5_1 with C; auto. eapply between_exchange4. apply H14. assumption. assert (Out B' A1 C1). eapply cong3_preserves_out. apply H13. unfold Cong_3. repeat split. apply cong_right_commutativity. eapply l2_11. apply H4. apply between_symmetry. apply H8. apply cong_symmetry. apply cong_left_commutativity. assumption. apply cong_right_commutativity. assumption; apply H8. apply cong_right_commutativity. eapply l2_11. apply H6. apply between_symmetry. apply H10. apply cong_symmetry. apply cong_left_commutativity. assumption. apply cong_right_commutativity. assumption. assumption. eapply l6_7. apply l6_6. eapply l6_7. apply H14. eapply l6_7. apply l6_6. apply H14. unfold Out. repeat split. intro. subst A1. unfold Out in H14. spliter. absurde. assumption. right. assumption. eapply l6_7. apply H14. unfold Out. repeat split. intro. subst C1. unfold Out in H14. spliter. absurde. assumption. right. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2