proposition: Lemma cp_max_min_to_p : forall l u x, cp_max l (cZ x) = cZ x -> cp_min (cZ x) u = cZ x-> to_p (l,u) x.
proof: Proof. intros [l | | ][u | | ]; unfold to_p; simpl; try(intros; auto; discriminate). intros x H1 H2; injection H1; injection H2; intros H3 H4;split; [rewrite <- H4; apply Z.le_max_l | rewrite <- H3; apply Z.le_min_r]. intros x H1 _ ; injection H1; intros H3;rewrite <- H3; apply Z.le_max_l. intros x _ H1; injection H1; intros H3; rewrite <- H3; apply Z.le_min_r. Qed.
imports: ZArith List Lia