proposition: Lemma lea_total : forall A B C D E F, A <> B -> B <> C -> D <> E -> E <> F -> LeA A B C D E F \/ LeA D E F A B C.
proof: Proof. intros A B C D E F HAB HBC HDE HEF. elim(col_dec A B C). { intro. elim(out_dec B A C). - intro; left; apply l11_31_1; auto. - intro; right; apply l11_31_2; auto; apply not_out_bet; auto. } intro. elim(col_dec D E F). { intro. elim(out_dec E D F). - intro; right; apply l11_31_1; auto. - intro; left; apply l11_31_2; auto; apply not_out_bet; auto. } intro. elim(lea_dec A B C D E F). intro; left; auto. intro HNlea. right. assert(HP := angle_construction_1 D E F A B C). destruct HP as [P []]; Col. exists P. split; auto. apply os2__inangle; Side. apply cop_nts__os; Col; Cop. - intro. apply HNlea. apply conga__lea. apply (l11_10 A B P D E F); try (apply out_trivial); try (apply conga_sym); auto. apply (col_one_side_out _ A); Col; Side. - intro. apply HNlea. apply (l11_30 A B C A B P); try (apply conga_refl); try (apply conga_sym); auto. exists C. split; try (apply conga_refl); auto. apply os_ts__inangle; Side. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2