proposition: Lemma osucc_inj : { when ordinalp &, injective osucc }.
proof: Proof. move=> a b oa ob eq. have /setU1_P [ab | //]: inc a (osucc b) by rewrite -eq; fprops. have /setU1_P [ba | //]: inc b (osucc a) by rewrite eq; fprops. case: (ordinal_irreflexive oa (ordinal_transitive oa ba ab)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)