proposition: Lemma Gamma0_epsilon: oopow Gamma_0 = Gamma_0.
proof: Proof. have [g1 g2] := Gamma0_p. have sa := (limit_pos (Gamma0_limit)). by move: (Sphi_p3 OS0 sa); rewrite g1 (Sphi_p0 (proj32_1 sa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)