X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2FQaxioms.ma;h=da8e9e7a6813904e229ca631b91490c35932e1af;hb=34d2f477be65e3fd26bfb6d43a3dd0807274549b;hp=6cf6b6994992d0cbdf7feda41d4cd892df836b22;hpb=962891404ac84c5f91425b89611ac9d8eca13f46;p=helm.git

diff --git a/helm/software/matita/library/Q/Qaxioms.ma b/helm/software/matita/library/Q/Qaxioms.ma
index 6cf6b6994..da8e9e7a6 100644
--- a/helm/software/matita/library/Q/Qaxioms.ma
+++ b/helm/software/matita/library/Q/Qaxioms.ma
@@ -65,7 +65,7 @@ axiom frac_Qinv1: \forall a,b:nat.Qinv(frac a b) = frac b a.
 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