fact: Definition interp (lvar : list (COLTpoint * positive)) (Default : COLTpoint) : positive -> COLTpoint := fun p => list_assoc_inv COLTpoint positive positive_dec lvar p Default.
imports: Recdef NArith GeoCoq.Utils.sets