proposition: Lemma opow_2int1 a b: a <o omega0 -> b <o omega0 -> (a ^o b) <o omega0.
proof: Proof. move /olt_omegaP => aN /olt_omegaP bN; apply /olt_omegaP. rewrite (opow_2int aN bN); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)