fact: Definition ble (N1 N2: zinf) : bool := match N1, N2 with _, Inf => true | Inf, _ => false | Fin h1, Fin h2 => h1 <=? h2 end.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)