proposition: Lemma nsv_lel a1 a2 b: a1 <=o a2 -> ordinalp b -> (S a1 b) <=o (S a2 b).
proof: Proof. move => leaa ob; case: (ole_eqVlt leaa). move ->;apply: oleR; apply:(OS_nsv (proj32 leaa) ob). move=> ltaa; exact:(proj1 (nsv_ltl ltaa ob)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)