fact: Definition meet (N1 N2: t) : t := {| low := Zinf.min (low N1) (low N2); high := Zinf.min (high N1) (high N2) |}.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)