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