proposition: Lemma conga_dec : forall A B C D E F, CongA A B C D E F \/ ~ CongA A B C D E F.
proof: Proof. intros. induction (eq_dec_points A B). subst;right;intro;unfold CongA in *;intuition. induction (eq_dec_points C B). subst;right;intro;unfold CongA in *;intuition. induction (eq_dec_points D E). subst;right;intro;unfold CongA in *;intuition. induction (eq_dec_points F E). subst;right;intro;unfold CongA in *;intuition. assert (exists A' : Tpoint, Bet B A A' /\ Cong A A' E D) by (apply segment_construction). decompose [ex and] H3; clear H3. assert (exists C' : Tpoint, Bet B C C' /\ Cong C C' E F) by (apply segment_construction). decompose [ex and] H3; clear H3. assert (exists D' : Tpoint, Bet E D D' /\ Cong D D' B A) by (apply segment_construction). decompose [ex and] H3; clear H3. assert (exists F' : Tpoint, Bet E F F' /\ Cong F F' B C) by (apply segment_construction). decompose [ex and] H3; clear H3. induction (cong_dec x x0 x1 x2). left. unfold CongA. repeat split; try assumption. exists x; exists x0; exists x1; exists x2. repeat split; assumption. right. unfold CongA. intro. decompose [and ex] H4; clear H4. assert (x3 = x) by (apply construction_uniqueness with B A E D; auto). assert (x4 = x0) by (apply construction_uniqueness with B C E F; auto). assert (x5 = x1) by (apply construction_uniqueness with E D B A; auto). assert (x6 = x2) by (apply construction_uniqueness with E F B C; auto). subst. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2