proposition: Lemma to_p_thinner : forall l u x, to_p (l,u) x -> thinner (l, cZ x) (l, u)/\ thinner (cZ x, u)(l,u).
proof: Proof. intros [l | |] [u | |] x ;unfold to_p, thinner; simpl; try(intuition;fail); repeat rewrite Zmin_idempotent; repeat rewrite Zmax_idempotent. intros; rewrite Z.max_comm; rewrite Zle_to_Zmax; try lia; rewrite Z.min_comm; rewrite Zle_to_Zmin; auto; lia. intros; rewrite Z.min_comm; rewrite Zle_to_Zmin; auto. intros; rewrite Z.max_comm; rewrite Zle_to_Zmax; auto. Qed.
imports: ZArith List Lia