fact: Definition add (N1 N2: t) : t := if isempty N1 || isempty N2 then bot else {| low := Zinf.add (low N1) (low N2); high := Zinf.add (high N1) (high N2) |}.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)