proposition: Lemma to_p_cp_max_min : forall l u x, to_p (l,u) x -> cp_max l (cZ x) = cZ x /\ cp_min (cZ x) u = cZ x.
proof: Proof. intros [l | | ][u | | ]; unfold to_p; simpl; try(intuition; fail). intros; rewrite Z.max_comm; rewrite Zle_to_Zmax;try rewrite Zle_to_Zmin; intuition. intros; rewrite Z.max_comm; rewrite Zle_to_Zmax; intuition. intros; rewrite Zle_to_Zmin; intuition. Qed.
imports: ZArith List Lia