proposition: Lemma conga_line : forall A B C A' B' C', A <> B -> B <> C -> A' <> B' -> B' <> C' -> Bet A B C -> Bet A' B' C' -> CongA A B C A' B' C'.
proof: Proof. intros. assert_diffs. prolong B C C0 B' C'. prolong B' C' C1 B C. prolong B A A0 B' A'. prolong B' A' A1 B A. unfold CongA. repeat split; try assumption. auto. auto. exists A0. exists C0. exists A1. exists C1. repeat split; try assumption. apply (l2_11 A0 B C0 A1 B' C1). eapply outer_transitivity_between2. apply between_symmetry. apply H11. eapply outer_transitivity_between. apply H3. assumption. assumption. assumption. eapply outer_transitivity_between2. apply between_symmetry. apply H13. eapply outer_transitivity_between. apply H4. assumption. assumption. assumption. apply cong_right_commutativity. eapply l2_11. apply between_symmetry. apply H11. apply H13. apply cong_left_commutativity. assumption. apply cong_symmetry. apply cong_right_commutativity. assumption. apply cong_right_commutativity. eapply l2_11. apply H7. apply between_symmetry. apply H9. apply cong_symmetry. apply cong_left_commutativity. assumption. apply cong_right_commutativity. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2