proposition: Lemma cong_dec_eq_dec : (forall A B C D, Cong A B C D \/ ~ Cong A B C D) -> (forall A B:Tpoint, A=B \/ A<>B).
proof: Proof. intros H A B. elim (H A B A A); intro HCong. left; apply cong_identity with A; assumption. right; intro; subst; apply HCong. apply cong_pseudo_reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le GeoCoq.Utils.all_equiv