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