proposition: Lemma EqT: transitive_r equipotent.
proof: Proof. move => c b a [f [bf sf tf]] [g [bg sg tg]]; exists (g \co f). split; aw => //. by apply: compose_fb => //; split => //; try fct_tac; rewrite tf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)