lemma 3.6 subverted

[helm.git] / helm / software / matita / library / Q / fraction / finv.ma

diff --git a/helm/software/matita/library/Q/fraction/finv.ma b/helm/software/matita/library/Q/fraction/finv.ma
index d9bf715b15d221f59b52d8149dddaece6e6d1fcf..2868bece0cd85f4d48217abbc0b3b16342cc68d1 100644 (file)
--- a/helm/software/matita/library/Q/fraction/finv.ma
+++ b/helm/software/matita/library/Q/fraction/finv.ma
@@ -32,7 +32,6 @@ theorem finv_finv: ∀f. finv (finv f) = f.
   ]
 qed.
 
-
 theorem or_numerator_nfa_one_nfa_proper: 
 ∀f.
  (numerator f = nfa_one ∧ ∃g.numerator (finv f) = nfa_proper g) ∨