proposition: Lemma l11_41 : forall A B C D, ~ Col A B C -> Bet B A D -> A <> D -> LtA A C B C A D /\ LtA A B C C A D.
proof: Proof. intros. split. apply l11_41_aux. assumption. assumption. assumption. prolong C A E C A. assert(LtA A B C B A E). eapply l11_41_aux. intro. apply H. apply col_permutation_5. assumption. assumption. assert_diffs;auto. assert(CongA B A C C A B). { apply conga_left_comm. apply conga_refl; assert_diffs;auto. } assert(CongA D A C E A B) by (eapply l11_13 with B C;assert_diffs;auto). unfold LtA in *. spliter. repeat split. apply l11_30 with A B C B A E; trivial. apply conga_refl;assert_diffs;auto. apply conga_sym. apply conga_comm. assumption. intro. apply H7. eapply conga_trans. apply H8. apply conga_comm. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2