fact: Definition ble (N1 N2: t) : bool := isempty N1 || (Zinf.ble (high N1) (high N2) && Zinf.ble (low N1) (low N2)).
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)