proposition: Lemma cp_min_assoc : forall a b c, cp_min (cp_min a b) c = cp_min a (cp_min b c).
proof: Proof. intros [a | | ]; simpl; auto; intros [b | |]; simpl; auto; intros [c| |]; simpl; auto. rewrite Z.min_assoc; auto. Qed.
imports: ZArith List Lia