proposition: Lemma coarserT: transitive_r coarser_cs.
proof: Proof. move=> z x y c1 c2 u uy. move: (c2 _ uy)=> [v zy uz]; move: (c1 _ zy)=> [t ty zt]. by ex_tac; apply: (sub_trans uz zt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)