proposition: Lemma axAODr s t u : mprv (u :/\: (s :\/: t) <--> u :/\: s :\/: u :/\: t).
proof: Proof. rule axEI. rule axAcase. rule axC. rule axOE; rule axC; [rewrite <- axOIl|rewrite <- axOIr];exact: axAI. rule axOE;[rewrite <- axOIl|rewrite <- axOIr]; exact: axI. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions