proposition: Lemma ord_negl_sum1 a b c: ordinalp a -> ordinalp b -> ordinalp c -> (a <<o c /\ b <<o c <-> (a +o b) <<o c).
proof: Proof. move => oa ob oc; rewrite /ord_negl - (osumA oa ob oc). split; first by move =>[h ->]. move => h. suff: b +o c = c by move => h1; rewrite -{2} h h1. apply:oleA (osum_M0le ob oc). by move: (osum_M0le oa (OS_sum2 ob oc)); rewrite h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)