proposition: Lemma ord_negl_trans a b c : ordinalp a -> ordinalp b -> ordinalp c -> a <<o b -> b <<o c -> a <<o c.
proof: Proof. by move => oa ob oc; rewrite /ord_negl => ab <-; rewrite osumA // ab. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)