axiom frac_Qinv2: \forall a,b:nat.Qinv(frac (Zopp a) b) = frac (Zopp b) a.
definition sigma_Q \def \lambda n,p,f.iter_p_gen n p Q f QO Qplus.
-
+(*
theorem geometric: \forall q.\exists k.
Qlt q (sigma_Q k (\lambda x.true) (\lambda x. frac (S O) x)).
-
\ No newline at end of file
+*)
\ No newline at end of file