proposition: Lemma rlt_leT b a c: a <r b -> b <=r c -> a <r c.
proof: Proof. move => [pa pb] pc;split; first exact: (rleT pa pc). move => ac; case: pb; apply:rleA => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)