proposition: Lemma set_leT: transitive_r set_le.
proof: Proof. move => y x z [f [fi sf tf]] [g [gi sg tg]]. exists (g \co f); saw; apply: (compose_fi fi gi);split; (try fct_tac); ue. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)