fact: Definition widen (i j:ext_Z*ext_Z) := let (bi, ui) := i in let (bj, uj) := j in let b := if ext_eq (cp_min bi bj) bi then bi else minfty in let u := if ext_eq (cp_max ui uj) ui then ui else pinfty in (b,u).
imports: ZArith List Lia