proposition: Lemma opowx1 x: ordinalp x -> x ^o \1o = x.
proof: Proof. have zno: \1o <> \0o by fprops. rewrite /opow; Ytac xz; [by Ytac0 |Ytac xno => // ]. move => ox;rewrite /opow' ord_induction_y1 oprod1l //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)