fact: Definition eq_ptr (x y : ptr) := match x, y with ptr_nat m, ptr_nat n => m == n end.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep