proposition: Lemma ole_ltT b a c: a <=o b -> b <o c -> a <o c.
proof: Proof. move=> ab [bc nbc]; split; first by apply: (oleT ab bc). by dneg ca; rewrite ca in ab; apply: oleA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)