proposition: Theorem equivalent_variants_of_line_circle : all_equiv (segment_circle:: one_point_line_circle:: two_points_line_circle:: nil).
proof: Proof. apply all_equiv__equiv; unfold all_equiv'; simpl; repeat split. rewrite segment_circle__one_point_line_circle, one_point_line_circle__two_points_line_circle; trivial. rewrite segment_circle__one_point_line_circle; trivial. rewrite one_point_line_circle__two_points_line_circle; trivial. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.sums GeoCoq.Utils.all_equiv