proposition: Lemma opow_2int a b: natp a ->natp b -> a ^o b = a ^c b.
proof: Proof. move=> aN bN;move: b bN. move: (OS_nat aN) => oa. apply: Nat_induction; first by rewrite cpowx0 opowx0. move=> n nN hrec. rewrite (cpow_succ _ nN) (succ_of_nat nN) (opow_succ oa (OS_nat nN)) hrec. apply: (oprod2_2int); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)