(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Q/Qaxioms".
-
include "Z/compare.ma".
include "Z/times.ma".
include "nat/iteration2.ma".
(*
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
+*)