proposition: Lemma cp_max_r_cp_min_l : forall a b, cp_max a b = b -> cp_min a b = a.
proof: Proof. intros [a | | ][b | | ]; simpl; auto. intros H; injection H; intros H1. assert (a <= b) by (rewrite <- H1; apply Z.le_max_l). rewrite Zle_to_Zmin; auto. Qed.
imports: ZArith List Lia