proposition: Theorem dirim_S f: {compat (direct_image f): u v / sub u v}.
proof: Proof. move=> u u' uu' t /dirim_P [x xu pr]; apply/dirim_P. by exists x => //;apply: uu'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)