proposition: Lemma l11_44_2_a : forall A B C, ~ Col A B C -> Lt B A B C -> LtA B C A B A C.
proof: Proof. intros. apply not_col_distincts in H. spliter. unfold Lt in H0. spliter. unfold Le in H0. ex_and H0 C'. assert(C <> C'). intro. subst C'. contradiction. assert(C' <> A). intro. subst C'. apply H. apply col_permutation_4. apply bet_col. assumption. assert(C' <> B). intro. subst C'. apply cong_identity in H5. subst A. absurde. assert(InAngle C' B A C). repeat split. auto. auto. assumption. exists C'. split. assumption. right. apply out_trivial. auto. assert(HH:=l11_41 C' C A B). assert(LtA C' A C A C' B /\ LtA C' C A A C' B). apply HH. intro. apply H. apply col_permutation_1. eapply col_transitivity_1. apply H6. apply col_permutation_4. assumption. apply col_permutation_3. apply bet_col. assumption. apply between_symmetry. assumption. assumption. clear HH. spliter. assert(LtA B A C' B A C). split. unfold LeA. exists C'. split. assumption. apply conga_refl. auto. assumption. intro. apply conga_os__out in H12. apply H. apply out_col in H12. apply bet_col in H0. apply col_permutation_1. eapply col_transitivity_1. apply H6. Col. Col. apply out_one_side. right. intro. apply H. Col. apply bet_out;auto. assert(LtA B C A A C' B). apply (conga_preserves_lta C' C A A C' B). apply out2__conga. apply l6_6. apply bet_out. auto. apply between_symmetry. assumption. apply out_trivial. auto. apply conga_refl; auto. assumption. assert(CongA B A C' B C' A). apply (l11_44_1_a A B C'); auto. apply conga_right_comm in H14. assert(LtA B C A B A C'). apply (conga_preserves_lta B C A A C' B). apply conga_refl; auto. apply conga_sym. assumption. assumption. eapply lta_trans. apply H15. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2