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