proposition: Lemma ax_conv_ch p q s : prv ([(p+q)^^]s <--> [p^^ + q^^]s).
proof: Proof. rewrite -> ax_Ch. rule axEI; first apply: rAI. - rewrite <- (ax_convEF (p+q) s) at 2. by rewrite -> ax_ChE, <- axOIl, <- (ax_convBB p [(p + q)^^]s). - rewrite <- (ax_convEF (p+q) s) at 2. by rewrite -> ax_ChE, <- axOIr, <- (ax_convBB q [(p + q)^^]s). - rewrite <- ax_Ch. rewrite -> (ax_convBB (p+q) [p^^ + q^^]s) at 1. apply: rNorm. rewrite -> ax_ChE,ax_Ch. rewrite -> axAEl at 1. rewrite -> axAEr. do ! rewrite -> ax_convEF. by rule axOE. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)