proposition: Lemma rev_pred_prop (f := osum2 \1o): normal_ofs f /\ (forall y, \0o <o y -> exists2 x, ordinalp x & y = f x).
proof: Proof. split; first apply: (osum_normal OS1). by move => y /ord_rev_pred [pa pb]; exists (y -o \1o); rewrite /f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)