proposition: Lemma cong_dec : forall A B C D, Cong A B C D \/ ~ Cong A B C D.
proof: Proof. intros. elim (eq_dec_points A B); intro; subst; elim (eq_dec_points C D); intro; subst. left; Cong. right; intro; apply H; apply cong_identity with B; Cong. right; intro; apply H; apply cong_identity with D; Cong. elim (segment_construction_2 B A C D). intros D' HD'. spliter. elim (eq_dec_points B D');intro. subst; left; assumption. right; intro. assert (Cong A D' A B) by CongR. elim H1; intro; clear H1. assert (B = D') by (apply (between_cong A D' B); Cong). subst;intuition. assert (D'=B) by (apply (between_cong A B D');assumption). subst;intuition. intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col