proposition: Lemma thinner_widen : forall v1 v2, thinner v1 (widen v1 v2).
proof: Proof. intros [[l1 | | ][u1 | | ]] [[l2 | | ][u2 | | ]]; try (unfold thinner, widen; intuition; fail); match goal with |- thinner (?x, ?y) (widen _ (?z, ?t)) => unfold thinner, widen; case (ext_eq (cp_min x z) x);case (ext_eq (cp_max y t) y); try rewrite cp_max_refl; try rewrite cp_min_refl; try (intuition; fail) end. Qed.
imports: ZArith List Lia