proposition: Lemma suppa_dec : forall A B C D E F, SuppA A B C D E F \/ ~ SuppA A B C D E F.
proof: Proof. intros. induction (eq_dec_points A B). right; intros []; auto. induction (eq_dec_points B C). right; intro Habs; apply suppa_distincts in Habs; spliter; auto. destruct (ex_suppa A B C) as [D' [E' [F']]]; auto. induction (conga_dec D' E' F' D E F). left; apply (conga2_suppa__suppa A B C D' E' F'); try apply conga_refl; auto. right; intro; apply H2, (suppa2__conga456 A B C); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2