proposition: Lemma l11_46 : forall A B C, A <> B -> B <> C -> (Per A B C \/ Obtuse A B C) -> Lt B A A C /\ Lt B C A C.
proof: Proof. intros. induction (col_dec A B C). induction H1. exfalso. apply (per_not_col A B C); auto. apply col_obtuse__bet in H1; auto. repeat split; Le. intro. apply H0, between_cong with A; Cong. intro. apply H, eq_sym, between_cong with C; Between; Cong. assert_diffs. assert(HH:= H1). apply l11_43 in H1; auto. spliter. split. apply lt_left_comm. apply l11_44_2_b. unfold Acute in H3. ex_and H3 A'. ex_and H4 B'. ex_and H3 C'. assert (Hd := H4). apply lta_distincts in Hd. spliter. induction HH. { eapply conga_preserves_lta with A C B A' B' C'. apply conga_refl;auto. apply l11_16;auto. apply lta_left_comm. assumption. } unfold Obtuse in H11. ex_and H11 A''. ex_and H12 B''. ex_and H11 C''. eapply lta_trans. apply lta_left_comm. apply H4. eapply conga_preserves_lta with A'' B'' C'' A B C. assert (Hd := H12). apply lta_distincts in Hd. spliter. apply l11_16; auto. apply conga_refl; auto. assumption. apply lt_left_comm. apply lt_right_comm. apply l11_44_2_b. unfold Acute in H1. ex_and H1 A'. ex_and H4 B'. ex_and H1 C'. assert (Hd := H4). apply lta_distincts in Hd. spliter. induction HH. eapply conga_preserves_lta. apply conga_refl; auto. apply l11_16. apply H1. auto. auto. apply l8_2. assumption. auto. auto. apply lta_left_comm. assumption. unfold Obtuse in H11. ex_and H11 A''. ex_and H12 B''. ex_and H11 C''. eapply lta_trans. apply lta_left_comm. apply H4. eapply conga_preserves_lta. apply lta_distincts in H12. spliter. apply (l11_16 A'' B'' C''); auto. apply conga_refl; auto. apply lta_right_comm. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2