fact: Definition add_test_constraint_left (d:bool) (i j:ext_Z*ext_Z) : option (ext_Z*ext_Z) := let (bi, ui):=i in let (bj, uj):=j in (if d then let bip1 := comp_add bi (cZ 1) in if ext_eq uj (cp_min bi uj) then None else Some (cp_max bip1 bj, uj) else let v := cp_max ui bj in if ext_eq bj v then if ext_eq ui v then Some(bj,cp_min ui uj) else None else Some (bj, cp_min ui uj)).
imports: ZArith List Lia