proposition: Lemma ord_negl_sum3 a b c: ordinalp c -> a <=o b -> b <<o c -> a <<o c.
proof: Proof. move => oc h1; move: (h1) => [oa _ _]. by move: (odiff_pr h1) => [od -> /(ord_negl_sum1 oa od oc) []]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)