proposition: Lemma ax_Ch p q s : prv ([p + q]s <--> ([p]s :/\: [q]s)).
proof: Proof. rule axEI. Intro. ApplyH axAI. ApplyH (axChEl p q s). ApplyH (axChEr p q s). rule axAcase. exact: axCh. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)