proposition: Lemma lea_dec : forall A B C D E F, LeA A B C D E F \/ ~ LeA A B C D E F.
proof: Proof. intros A B C D E F. elim(eq_dec_points A B). intro; right; intro Hlea; apply lea_distincts in Hlea; spliter; auto. intro. elim(eq_dec_points B C). intro; right; intro Hlea; apply lea_distincts in Hlea; spliter; auto. intro. elim(eq_dec_points D E). intro; right; intro Hlea; apply lea_distincts in Hlea; spliter; auto. intro. elim(eq_dec_points E F). intro; right; intro Hlea; apply lea_distincts in Hlea; spliter; auto. intro. elim(col_dec A B C). { intro. elim(out_dec B A C). intro; left; apply l11_31_1; auto. intro. elim(bet_dec D E F). intro; left; apply l11_31_2; auto. intro HENBet. right. intro. apply HENBet. apply (bet_lea__bet A B C); auto. apply not_out_bet; auto. } intro HNColB. elim(col_dec D E F). { intro. elim(bet_dec D E F). intro; left; apply l11_31_2; auto. intro. right. intro. apply HNColB. apply col_permutation_4. apply out_col. apply (out_lea__out _ _ _ D E F); auto. apply not_bet_out; auto. } intro. assert(HP := angle_construction_1 A B C D E F). destruct HP as [P []]; Col. elim(inangle_dec D E F P). intro; left; exists P; auto. intro HNInAngle. right. intro. apply HNInAngle. apply lea_in_angle; try (apply conga_sym); Side. apply (l11_30 A B C D E F); auto; apply conga_refl; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2