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