proposition: Theorem equivalence_between_decidability_properties_of_basic_relations : all_equiv (decidability_of_equality_of_points:: decidability_of_congruence_of_points:: decidability_of_betweenness_of_points::nil).
proof: Proof. apply all_equiv__equiv. simpl. unfold decidability_of_equality_of_points, decidability_of_congruence_of_points, decidability_of_betweenness_of_points. assert (P:=cong_dec_eq_dec). assert (Q:=eq_dec_cong_dec). assert (R:=bet_dec_eq_dec). assert (S:=eq_dec_bet_dec). repeat split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le GeoCoq.Utils.all_equiv