Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective