proposition: Lemma hint_box_con p0 p1 s b : ([p0;;p1]s, b) \in C -> ([p0][p1]s, b) \in C.
proof: Proof. case/andP: hint_C => _ /allP H inC. by move: (H _ inC). Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)