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