proposition: Lemma eq_dec_F : forall A B, EqF A B \/ ~ EqF A B.
proof: Proof. intros; unfold EqF; simpl. destruct A as [A HA]; destruct B as [B HB]; simpl. exact (eq_dec_points A B). Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems