proposition: Lemma fun_trans x y z : fun_leq x y -> fun_leq y z -> fun_leq x z.
proof: Proof. by move=>H1 H2 t; apply: poset_trans (H2 t). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)