  In 1926-1927, Tarski designed a set of axioms for Euclidean geometry which
reached its final form in a manuscript by Schwabh\"auser, Szmielew and Tarski
in 1983. The differences amount to simplifications obtained by Tarski and
Gupta. Gupta presented an independent version of Tarski's system of geometry,
thus establishing that his version could not be further simplified without
modifying the axioms. To obtain the independence of one of his axioms, namely
Pasch's axiom, he proved the independence of one of its consequences: the
previously eliminated symmetry of betweenness. However, an independence model
for the non-degenerate part of Pasch's axiom was provided by Szczerba for
another version of Tarski's system of geometry in which the symmetry of
betweenness holds. This independence proof cannot be directly used for Gupta's
version as the statements of the parallel postulate differ.
  In this paper, we present our progress towards obtaining an independent
version of a variant of Gupta's system. Compared to Gupta's version, we split
Pasch's axiom into this previously eliminated axiom and its non-degenerate part
and change the statement of the parallel postulate. We verified the
independence properties by mechanizing counter-models using the Coq
proof-assistant.
