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