proposition: Theorem equivalent_variants_of_circle_circle : all_equiv (circle_circle:: circle_circle_two:: circle_circle_bis:: circle_circle_axiom:: euclid_s_prop_1_22:: nil).
proof: Proof. assert (V := circle_circle_bis__circle_circle_axiom). assert (W := circle_circle__circle_circle_bis). assert (X := circle_circle__circle_circle_two). assert (Y := circle_circle_bis__euclid_22). assert (Z := euclid_22__circle_circle). apply all_equiv__equiv; unfold all_equiv'; simpl; repeat split; tauto. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.sums GeoCoq.Utils.all_equiv