proposition: Lemma nsv_ler a b1 b2: ordinalp a -> b1 <=o b2 -> (S a b1) <=o (S a b2).
proof: Proof. move => oa lt1; rewrite (nsvC oa (proj31 lt1))(nsvC oa (proj32 lt1)). by apply:nsv_lel. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)