Theory Integer_Hull
section ‹Integer Hull›
text ‹We define the integer hull of a polyhedron, i.e., the convex hull of all integer solutions.
Moreover, we prove the result of Meyer that the integer hull of a polyhedron defined by an
integer matrix is again a polyhedron, and give bounds for a corresponding decomposition theorem.›
theory Integer_Hull
imports
Decomposition_Theorem
Mixed_Integer_Solutions
begin
context gram_schmidt
begin
definition "integer_hull P = convex_hull (P ∩ ℤ⇩v)"
lemma integer_hull_mono: "P ⊆ Q ⟹ integer_hull P ⊆ integer_hull Q"
unfolding integer_hull_def
by (intro convex_hull_mono, auto)
end
lemma abs_neg_floor: "¦of_int b¦ ≤ Bnd ⟹ - (floor Bnd) ≤ b"
using abs_le_D2 floor_mono by fastforce
lemma abs_pos_floor: "¦of_int b¦ ≤ Bnd ⟹ b ≤ floor Bnd"
using abs_le_D1 le_floor_iff by auto
context gram_schmidt_floor
begin
lemma integer_hull_integer_cone: assumes C: "C ⊆ carrier_vec n"
and CI: "C ⊆ ℤ⇩v"
shows "integer_hull (cone C) = cone C"
proof
have "cone C ∩ ℤ⇩v ⊆ cone C" by blast
thus "integer_hull (cone C) ⊆ cone C"
using cone_cone[OF C] convex_cone[OF C] convex_hull_mono
unfolding integer_hull_def convex_def by metis
{
fix x
assume "x ∈ cone C"
then obtain D where finD: "finite D" and DC: "D ⊆ C" and x: "x ∈ finite_cone D"
unfolding cone_def by auto
from DC C CI have D: "D ⊆ carrier_vec n" and DI: "D ⊆ ℤ⇩v" by auto
from D x finD have "x ∈ finite_cone (D ∪ {0⇩v n})" using finite_cone_mono[of "D ∪ {0⇩v n}" D] by auto
then obtain l where x: "lincomb l (D ∪ {0⇩v n}) = x"
and l: "l ` (D ∪ {0⇩v n}) ⊆ {t. t ≥ 0}"
using finD unfolding finite_cone_def nonneg_lincomb_def by auto
define L where "L = sum l (D ∪ {0⇩v n})"
define L_sup :: 'a where "L_sup = of_int (floor L + 1)"
have "L_sup ≥ L" using floor_correct[of L] unfolding L_sup_def by linarith
have "L ≥ 0" unfolding L_def using sum_nonneg[of _ l] l by blast
hence "L_sup ≥ 1" unfolding L_sup_def by simp
hence "L_sup > 0" by fastforce
let ?f = "λ y. if y = 0⇩v n then L_sup - L else 0"
have "lincomb ?f {0⇩v n} = 0⇩v n"
using already_in_span[of "{}" "0⇩v n"] lincomb_in_span local.span_empty
by auto
moreover have "lincomb ?f (D - {0⇩v n}) = 0⇩v n"
by(rule lincomb_zero, insert D, auto)
ultimately have "lincomb ?f (D ∪ {0⇩v n}) = 0⇩v n"
using lincomb_vec_diff_add[of "D ∪ {0⇩v n}" "{0⇩v n}"] D finD by simp
hence lcomb_f: "lincomb (λ y. l y + ?f y) (D ∪ {0⇩v n}) = x"
using lincomb_sum[of "D ∪ {0⇩v n}" l ?f] finD D x by simp
have "sum ?f (D ∪ {0⇩v n}) = L_sup - L"
by (simp add: sum.subset_diff[of "{0⇩v n}" "D ∪ {0⇩v n}" ?f] finD)
hence "sum (λ y. l y + ?f y) (D ∪ {0⇩v n}) = L_sup"
using l L_def by auto
moreover have "(λ y. l y + ?f y) ` (D ∪ {0⇩v n}) ⊆ {t. t ≥ 0}"
using ‹L ≤ L_sup› l by force
ultimately obtain l' where x: "lincomb l' (D ∪ {0⇩v n}) = x"
and l': "l' ` (D ∪ {0⇩v n}) ⊆ {t. t ≥ 0}"
and sum_l': "sum l' (D ∪ {0⇩v n}) = L_sup"
using lcomb_f by blast
let ?D' = "{L_sup ⋅⇩v v | v. v ∈ D ∪ {0⇩v n}}"
have Did: "?D' = (λ v. L_sup ⋅⇩v v) ` (D ∪ {0⇩v n})" by force
define l'' where "l'' = (λ y. l' ((1 / L_sup) ⋅⇩v y) / L_sup)"
obtain lD where dist: "distinct lD" and lD: "D ∪ {0⇩v n} = set lD"
using finite_distinct_list[of "D ∪ {0⇩v n}"] finD by auto
let ?lD' = "map ((⋅⇩v) L_sup) lD"
have dist': "distinct ?lD'"
using distinct_smult_nonneg[OF _ dist] ‹L_sup > 0› by fastforce
have x': "lincomb l'' ?D' = x" unfolding x[symmetric] l''_def
unfolding lincomb_def Did
proof (subst finsum_reindex)
from ‹L_sup > 0› smult_vec_nonneg_eq[of L_sup] show "inj_on ((⋅⇩v) L_sup) (D ∪ {0⇩v n})"
by (auto simp: inj_on_def)
show "(λv. l' (1 / L_sup ⋅⇩v v) / L_sup ⋅⇩v v) ∈ (⋅⇩v) L_sup ` (D ∪ {0⇩v n}) → carrier_vec n"
using D by auto
from ‹L_sup > 0› have "L_sup ≠ 0" by auto
then show "(⨁⇘V⇙x∈D ∪ {0⇩v n}. l' (1 / L_sup ⋅⇩v (L_sup ⋅⇩v x)) / L_sup ⋅⇩v (L_sup ⋅⇩v x)) =
(⨁⇘V⇙v∈D ∪ {0⇩v n}. l' v ⋅⇩v v)"
by (intro finsum_cong, insert D, auto simp: smult_smult_assoc)
qed
have "D ∪ {0⇩v n} ⊆ cone C" using set_in_cone[OF C] DC zero_in_cone by blast
hence D': "?D' ⊆ cone C" using cone_smult[of L_sup, OF _ C] ‹L_sup > 0› by auto
have "D ∪ {0⇩v n} ⊆ ℤ⇩v" unfolding zero_vec_def using DI Ints_vec_def by auto
moreover have "L_sup ∈ ℤ" unfolding L_sup_def by auto
ultimately have D'I: "?D' ⊆ ℤ⇩v" unfolding Ints_vec_def by force
have "1 = sum l' (D ∪ {0⇩v n}) * (1 / L_sup)" using sum_l' ‹L_sup > 0› by auto
also have "sum l' (D ∪ {0⇩v n}) = sum_list (map l' lD)"
using sum.distinct_set_conv_list[OF dist] lD by auto
also have "map l' lD = map (l' ∘ ((⋅⇩v) (1 / L_sup))) ?lD'"
using smult_smult_assoc[of "1 / L_sup" L_sup] ‹L_sup > 0›
by (simp add: comp_assoc)
also have "l' ∘ ((⋅⇩v) (1 / L_sup)) = (λ x. l' ((1 / L_sup) ⋅⇩v x))" by (rule comp_def)
also have "sum_list (map … ?lD') * (1 / L_sup) =
sum_list (map (λy. l' (1 / L_sup ⋅⇩v y) * (1 / L_sup)) ?lD')"
using sum_list_mult_const[of _ "1 / L_sup" ?lD'] by presburger
also have "… = sum_list (map l'' ?lD')"
unfolding l''_def using ‹L_sup > 0› by simp
also have "… = sum l'' (set ?lD')" using sum.distinct_set_conv_list[OF dist'] by metis
also have "set ?lD' = ?D'" using lD by auto
finally have sum_l': "sum l'' ?D' = 1" by auto
moreover have "l'' ` ?D' ⊆ {t. t ≥ 0}"
proof
fix y
assume "y ∈ l'' ` ?D'"
then obtain x where y: "y = l'' x" and "x ∈ ?D'" by blast
then obtain v where "v ∈ D ∪ {0⇩v n}" and x: "x = L_sup ⋅⇩v v" by blast
hence "0 ≤ l' v / L_sup" using l' ‹L_sup > 0› by fastforce
also have "… = l'' x" unfolding x l''_def
using smult_smult_assoc[of "1 / L_sup" "L_sup" v] ‹L_sup > 0› by simp
finally show "y ∈ {t. t ≥ 0}" using y by blast
qed
moreover have "finite ?D'" using finD by simp
ultimately have "x ∈ integer_hull (cone C)"
unfolding integer_hull_def convex_hull_def
using x' D' D'I convex_lincomb_def[of l'' ?D' x]
nonneg_lincomb_def[of l'' ?D' x] by fast
}
thus "cone C ⊆ integer_hull (cone C)" by blast
qed
theorem decomposition_theorem_integer_hull_of_polyhedron:
assumes db: "is_det_bound db"
and A: "A ∈ carrier_mat nr n"
and b: "b ∈ carrier_vec nr"
and AI: "A ∈ ℤ⇩m"
and bI: "b ∈ ℤ⇩v"
and P: "P = polyhedron A b"
and Bnd: "of_int Bnd ≥ Max (abs ` (elements_mat A ∪ vec_set b))"
shows "∃ H C. H ∪ C ⊆ carrier_vec n ∩ ℤ⇩v
∧ H ⊆ Bounded_vec (of_nat (n + 1) * of_int (db n (max 1 Bnd)))
∧ C ⊆ Bounded_vec (of_int (db n (max 1 Bnd)))
∧ finite (H ∪ C)
∧ integer_hull P = convex_hull H + cone C"
proof -
define MBnd where "MBnd = Max (abs ` (elements_mat A ∪ set⇩v b))"
define DBnd :: 'a where "DBnd = of_int (db n (max 1 Bnd))"
define nBnd where "nBnd = of_nat (n+1) * DBnd"
have DBnd0: "DBnd ≥ 0" unfolding DBnd_def of_int_0_le_iff
by (rule is_det_bound_ge_zero[OF db], auto)
have Pn: "P ⊆ carrier_vec n" unfolding P polyhedron_def by auto
have "A ∈ Bounded_mat MBnd ∧ b ∈ Bounded_vec MBnd"
unfolding MBnd_def Bounded_mat_elements_mat Bounded_vec_vec_set
by (intro ballI conjI Max_ge finite_imageI imageI finite_UnI, auto)
hence "A ∈ Bounded_mat (of_int Bnd) ∧ b ∈ Bounded_vec (of_int Bnd)"
using Bounded_mat_mono[OF Bnd] Bounded_vec_mono[OF Bnd] unfolding MBnd_def by auto
from decomposition_theorem_polyhedra_1[OF A b P, of db Bnd] db AI bI this
obtain QQ Q C where C: "C ⊆ carrier_vec n" and finC: "finite C"
and QQ: "QQ ⊆ carrier_vec n" and finQ: "finite QQ" and BndQQ: "QQ ⊆ Bounded_vec DBnd"
and P: "P = Q + cone C"
and Q_def: "Q = convex_hull QQ"
and CI: "C ⊆ ℤ⇩v" and BndC: "C ⊆ Bounded_vec DBnd"
by (auto simp: DBnd_def)
define Bnd' where "Bnd' = of_nat n * DBnd"
note coneC = cone_iff_finite_cone[OF C finC]
have Q: "Q ⊆ carrier_vec n" unfolding Q_def using convex_hull_carrier[OF QQ] .
define B where "B = {x. ∃ a D. nonneg_lincomb a D x ∧ D ⊆ C ∧ lin_indpt D ∧ (∀ d ∈ D. a d ≤ 1)}"
{
fix b
assume "b ∈ B"
then obtain a D where b: "b = lincomb a D" and DC: "D ⊆ C"
and linD: "lin_indpt D" and bnd_a: "∀ d ∈ D. 0 ≤ a d ∧ a d ≤ 1"
by (force simp: B_def nonneg_lincomb_def)
from DC C have D: "D ⊆ carrier_vec n" by auto
from DC finC have finD: "finite D" by (metis finite_subset)
from D linD finD have cardD: "card D ≤ n" using dim_is_n li_le_dim(2) by auto
from BndC DC have BndD: "D ⊆ Bounded_vec DBnd" by auto
from lincomb_card_bound[OF this D DBnd0 _ cardD, of a, folded b] bnd_a
have "b ∈ Bounded_vec Bnd'" unfolding Bnd'_def by force
}
hence BndB: "B ⊆ Bounded_vec Bnd'" ..
from BndQQ have BndQ: "Q ⊆ Bounded_vec DBnd" unfolding Q_def using QQ by (metis convex_hull_bound)
have B: "B ⊆ carrier_vec n"
unfolding B_def nonneg_lincomb_def using C by auto
from Q B have QB: "Q + B ⊆ carrier_vec n" by (auto elim!: set_plus_elim)
from sum_in_Bounded_vecI[of _ DBnd _ Bnd' n] BndQ BndB B Q
have "Q + B ⊆ Bounded_vec (DBnd + Bnd')" by (auto elim!: set_plus_elim)
also have "DBnd + Bnd' = nBnd" unfolding nBnd_def Bnd'_def by (simp add: algebra_simps)
finally have QB_Bnd: "Q + B ⊆ Bounded_vec nBnd" by blast
have finQBZ: "finite ((Q + B) ∩ ℤ⇩v)"
proof (rule finite_subset[OF subsetI])
define ZBnd where "ZBnd = floor nBnd"
let ?vecs = "set (map vec_of_list (concat_lists (map (λ i. map (of_int :: _ ⇒ 'a) [-ZBnd..ZBnd]) [0..<n])))"
have id: "?vecs = vec_of_list `
{as. length as = n ∧ (∀i<n. ∃ b. as ! i = of_int b ∧ b ∈ {- ZBnd..ZBnd})}"
unfolding set_map by (rule image_cong, auto)
show "finite ?vecs" by (rule finite_set)
fix x
assume "x ∈ (Q + B) ∩ ℤ⇩v"
hence xQB: "x ∈ Q + B" and xI: "x ∈ ℤ⇩v" by auto
from xQB QB_Bnd QB have xBnd: "x ∈ Bounded_vec nBnd" and x: "x ∈ carrier_vec n" by auto
have xid: "x = vec_of_list (list_of_vec x)" by auto
show "x ∈ ?vecs" unfolding id
proof (subst xid, intro imageI CollectI conjI allI impI)
show "length (list_of_vec x) = n" using x by auto
fix i
assume i: "i < n"
have id: "list_of_vec x ! i = x $ i" using i x by auto
from xBnd[unfolded Bounded_vec_def] i x have xiBnd: "abs (x $ i) ≤ nBnd" by auto
from xI[unfolded Ints_vec_def] i x have "x $ i ∈ ℤ" by auto
then obtain b where b: "x $ i = of_int b" unfolding Ints_def by blast
show "∃b. list_of_vec x ! i = of_int b ∧ b ∈ {- ZBnd..ZBnd}" unfolding id ZBnd_def
using xiBnd unfolding b by (intro exI[of _ b], auto intro!: abs_neg_floor abs_pos_floor)
qed
qed
have QBZ: "(Q + B) ∩ ℤ⇩v ⊆ carrier_vec n" using QB by auto
from decomposition_theorem_polyhedra_2[OF QBZ finQBZ, folded integer_hull_def, OF C finC refl]
obtain A' b' nr' where A': "A' ∈ carrier_mat nr' n" and b': "b' ∈ carrier_vec nr'"
and IH: "integer_hull (Q + B) + cone C = polyhedron A' b'"
by auto
{
fix p
assume "p ∈ P ∩ ℤ⇩v"
hence pI: "p ∈ ℤ⇩v" and p: "p ∈ Q + cone C" unfolding P by auto
from set_plus_elim[OF p] obtain q c where
pqc: "p = q + c" and qQ: "q ∈ Q" and cC: "c ∈ cone C" by auto
from qQ Q have q: "q ∈ carrier_vec n" by auto
from Caratheodory_theorem[OF C] cC
obtain D where cD: "c ∈ finite_cone D" and DC: "D ⊆ C" and linD: "lin_indpt D" by auto
from DC C have D: "D ⊆ carrier_vec n" by auto
from DC finC have finD: "finite D" by (metis finite_subset)
from cD finD
obtain a where "nonneg_lincomb a D c" unfolding finite_cone_def by auto
hence caD: "c = lincomb a D" and a0: "⋀ d. d ∈ D ⟹ a d ≥ 0"
unfolding nonneg_lincomb_def by auto
define a1 where "a1 = (λ c. a c - of_int (floor (a c)))"
define a2 where "a2 = (λ c. of_int (floor (a c)) :: 'a)"
define d where "d = lincomb a2 D"
define b where "b = lincomb a1 D"
have b: "b ∈ carrier_vec n" and d: "d ∈ carrier_vec n" unfolding d_def b_def using D by auto
have bB: "b ∈ B" unfolding B_def b_def nonneg_lincomb_def
proof (intro CollectI exI[of _ a1] exI[of _ D] conjI ballI refl subsetI linD)
show "x ∈ a1 ` D ⟹ 0 ≤ x" for x using a0 unfolding a1_def by auto
show "a1 c ≤ 1" for c unfolding a1_def by linarith
qed (insert DC, auto)
have cbd: "c = b + d" unfolding b_def d_def caD lincomb_sum[OF finD D, symmetric]
by (rule lincomb_cong[OF refl D], auto simp: a1_def a2_def)
have "nonneg_lincomb a2 D d" unfolding d_def nonneg_lincomb_def
by (intro allI conjI refl subsetI, insert a0, auto simp: a2_def)
hence dC: "d ∈ cone C" unfolding cone_def finite_cone_def using finC finD DC by auto
have p: "p = (q + b) + d" unfolding pqc cbd using q b d by auto
have dI: "d ∈ ℤ⇩v" using CI DC C unfolding d_def indexed_Ints_vec_UNIV
by (intro lincomb_indexed_Ints_vec, auto simp: a2_def)
from diff_indexed_Ints_vec[of _ _ _ UNIV, folded indexed_Ints_vec_UNIV, OF _ d pI dI, unfolded p]
have "q + b + d - d ∈ ℤ⇩v" using q b d by auto
also have "q + b + d - d = q + b" using q b d by auto
finally have qbI: "q + b ∈ ℤ⇩v" by auto
have "p ∈ integer_hull (Q + B) + cone C" unfolding p integer_hull_def
by (intro set_plus_intro dC set_mp[OF set_in_convex_hull] IntI qQ bB qbI, insert Q B,
auto elim!: set_plus_elim)
}
hence "P ∩ ℤ⇩v ⊆ integer_hull (Q + B) + cone C" by auto
hence one_dir: "integer_hull P ⊆ integer_hull (Q + B) + cone C" unfolding IH
unfolding integer_hull_def using convex_convex_hull[OF polyhedra_are_convex[OF A' b' refl]]
convex_hull_mono by blast
have "integer_hull (Q + B) + cone C ⊆ integer_hull P + cone C" unfolding P
proof (intro set_plus_mono2 subset_refl integer_hull_mono)
show "B ⊆ cone C" unfolding B_def cone_def finite_cone_def using finite_subset[OF _ finC] by auto
qed
also have "… = integer_hull P + integer_hull (cone C)"
using integer_hull_integer_cone[OF C CI] by simp
also have "… = convex_hull (P ∩ ℤ⇩v) + convex_hull (cone C ∩ ℤ⇩v)"
unfolding integer_hull_def by simp
also have "… = convex_hull ((P ∩ ℤ⇩v) + (cone C ∩ ℤ⇩v))"
by (rule convex_hull_sum[symmetric], insert Pn cone_carrier[OF C], auto)
also have "… ⊆ convex_hull ((P + cone C) ∩ ℤ⇩v)"
proof (rule convex_hull_mono)
show "P ∩ ℤ⇩v + cone C ∩ ℤ⇩v ⊆ (P + cone C) ∩ ℤ⇩v"
using add_indexed_Ints_vec[of _ n _ UNIV, folded indexed_Ints_vec_UNIV] cone_carrier[OF C] Pn
by (auto elim!: set_plus_elim)
qed
also have "… = integer_hull (P + cone C)" unfolding integer_hull_def ..
also have "P + cone C = P"
proof -
have CC: "cone C ⊆ carrier_vec n" using C by (rule cone_carrier)
have "P + cone C = Q + (cone C + cone C)" unfolding P
by (rule assoc_add_vecset[symmetric, OF Q CC CC])
also have "cone C + cone C = cone C" by (rule cone_add_cone[OF C])
finally show ?thesis unfolding P .
qed
finally have "integer_hull (Q + B) + cone C ⊆ integer_hull P" .
with one_dir have id: "integer_hull P = integer_hull (Q + B) + cone C" by auto
show ?thesis unfolding id unfolding integer_hull_def DBnd_def[symmetric] nBnd_def[symmetric]
proof (rule exI[of _ "(Q + B) ∩ ℤ⇩v"], intro exI[of _ C] conjI refl BndC)
from QB_Bnd show "(Q + B) ∩ ℤ⇩v ⊆ Bounded_vec nBnd" by auto
show "(Q + B) ∩ ℤ⇩v ∪ C ⊆ carrier_vec n ∩ ℤ⇩v"
using QB C CI by auto
show "finite ((Q + B) ∩ ℤ⇩v ∪ C)" using finQBZ finC by auto
qed
qed
corollary integer_hull_of_polyhedron: assumes A: "A ∈ carrier_mat nr n"
and b: "b ∈ carrier_vec nr"
and AI: "A ∈ ℤ⇩m"
and bI: "b ∈ ℤ⇩v"
and P: "P = polyhedron A b"
shows "∃ A' b' nr'. A' ∈ carrier_mat nr' n ∧ b' ∈ carrier_vec nr' ∧
integer_hull P = polyhedron A' b'"
proof -
obtain Bnd where Bnd: "Max (abs ` (elements_mat A ∪ set⇩v b)) ≤ of_int Bnd"
by (meson ex_le_of_int)
from decomposition_theorem_integer_hull_of_polyhedron[OF det_bound_fact A b AI bI P Bnd]
obtain H C
where HC: "H ∪ C ⊆ carrier_vec n ∩ ℤ⇩v" "finite (H ∪ C)"
and decomp: "integer_hull P = convex_hull H + cone C" by auto
show ?thesis
by (rule decomposition_theorem_polyhedra_2[OF _ _ _ _ decomp], insert HC, auto)
qed
corollary small_integer_solution_nonstrict_via_decomp: fixes A :: "'a mat"
assumes db: "is_det_bound db"
and A: "A ∈ carrier_mat nr n"
and b: "b ∈ carrier_vec nr"
and AI: "A ∈ ℤ⇩m"
and bI: "b ∈ ℤ⇩v"
and Bnd: "of_int Bnd ≥ Max (abs ` (elements_mat A ∪ vec_set b))"
and x: "x ∈ carrier_vec n"
and xI: "x ∈ ℤ⇩v"
and sol: "A *⇩v x ≤ b"
shows "∃ y.
y ∈ carrier_vec n ∧
y ∈ ℤ⇩v ∧
A *⇩v y ≤ b ∧
y ∈ Bounded_vec (of_nat (n+1) * of_int (db n (max 1 Bnd)))"
proof -
from x sol have "x ∈ polyhedron A b" unfolding polyhedron_def by auto
with xI x have xsol: "x ∈ integer_hull (polyhedron A b)" unfolding integer_hull_def
by (meson IntI convex_hull_mono in_mono inf_sup_ord(1) inf_sup_ord(2) set_in_convex_hull)
from decomposition_theorem_integer_hull_of_polyhedron[OF db A b AI bI refl Bnd]
obtain H C where HC: "H ∪ C ⊆ carrier_vec n ∩ ℤ⇩v"
"H ⊆ Bounded_vec (of_nat (n + 1) * of_int (db n (max 1 Bnd)))"
"finite (H ∪ C)" and
id: "integer_hull (polyhedron A b) = convex_hull H + cone C"
by auto
from xsol[unfolded id] have "H ≠ {}" unfolding set_plus_def by auto
then obtain h where hH: "h ∈ H" by auto
with set_in_convex_hull have "h ∈ convex_hull H" using HC by auto
moreover have "0⇩v n ∈ cone C" by (intro zero_in_cone)
ultimately have "h + 0⇩v n ∈ integer_hull (polyhedron A b)" unfolding id by auto
also have "h + 0⇩v n = h" using hH HC by auto
also have "integer_hull (polyhedron A b) ⊆ convex_hull (polyhedron A b)"
unfolding integer_hull_def by (rule convex_hull_mono, auto)
also have "convex_hull (polyhedron A b) = polyhedron A b" using A b
using convex_convex_hull polyhedra_are_convex by blast
finally have h: "h ∈ carrier_vec n" "A *⇩v h ≤ b" unfolding polyhedron_def by auto
show ?thesis
by (intro exI[of _ h] conjI h, insert HC hH, auto)
qed
lemmas small_integer_solution_nonstrict_via_decomp_hadamard =
small_integer_solution_nonstrict_via_decomp[OF det_bound_hadamard, unfolded det_bound_hadamard_def]
end
end