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