proposition: Lemma Rpos a s C : s^- \notin R a C.
proof: Proof. apply/negP. case/fimsetP => t. rewrite inE andbC. by case (isBoxP a t) => // t' ->. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)