fact: Definition inv_rel := forall a1 a2 a', valid (a1 \+ a2 \+ a') -> D a1 (a2 \+ a') -> D a2 (a1 \+ a') -> D a1 a2 && D (a1 \+ a2) a'.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype) pcm(options axioms prelude) pcm(pcm morphism)