proposition: Lemma opow_Mlele x x' y y': x <> \0o -> x <=o x' -> y <=o y' -> (x ^o y) <=o (x' ^o y').
proof: Proof. move=> xnz xx' yy'. have [ox ox' _] := xx'. have oy':=(proj32 yy'). case: (ord2_trichotomy ox) => // x2. rewrite x2 opow1x; apply: oge1; fprops => h. move: (opow_nz0 ox' oy' h) => [p1 p2]. by rewrite p1 in xx'; move: (ole0 xx'). move: ord_pow_axioms => [ax1 _ _ _ ]. move: (ord_induction_p16 (erefl opow') ax1 x2 xx' yy'). by rewrite - (opow2x _ x2) - (opow2x _ (oleT x2 xx')). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)