proposition: Lemma ord_negl_sum' a b c: ordinalp a -> a <<o b -> b <=o c -> a <<o c.
proof: Proof. move => oa lab h1; move: (h1) => [ob oc _]. move: (odiff_pr h1) => [od -> ]; apply: (ord_negl_sum oa ob od lab). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)