X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Ffraction%2Ffraction.ma;h=ba4b417f6c2b6d067b2e1c331eaa8e87ee60e12f;hb=f524a0d716de2bdc0874aace8f82f6289034eccf;hp=81b60de91fc924a0e3d10214d920c00fb461b123;hpb=13ee180b4b982b7a150e8d727ed4b83813ac3fa2;p=helm.git

diff --git a/helm/software/matita/library/Q/fraction/fraction.ma b/helm/software/matita/library/Q/fraction/fraction.ma
index 81b60de91..ba4b417f6 100644
--- a/helm/software/matita/library/Q/fraction/fraction.ma
+++ b/helm/software/matita/library/Q/fraction/fraction.ma
@@ -29,56 +29,6 @@ let rec nat_fact_to_fraction n ≝
   | nf_cons m l ⇒ cons (Z_of_nat m) (nat_fact_to_fraction l)
   ].
 
-(* returns the numerator of a fraction in the form of a nat_fact_all *)
-let rec numerator f \def
-  match f with
-  [pp a \Rightarrow nfa_proper (nf_last a)
-  |nn a \Rightarrow nfa_one
-  |cons a l \Rightarrow
-    let n \def numerator l in
-    match n with
-    [nfa_zero \Rightarrow (* this case is vacuous *) nfa_zero
-    |nfa_one  \Rightarrow
-      match a with 
-      [OZ \Rightarrow nfa_one
-      |pos x \Rightarrow nfa_proper (nf_last x)
-      |neg x \Rightarrow nfa_one
-      ]
-    |nfa_proper g \Rightarrow
-      match a with 
-      [OZ \Rightarrow nfa_proper (nf_cons O g)
-      |pos x \Rightarrow nfa_proper (nf_cons (S x) g)
-      |neg x \Rightarrow nfa_proper (nf_cons O g)
-      ]
-    ]
-  ].
-
-theorem not_eq_numerator_nfa_zero: 
-\forall f.numerator f \neq nfa_zero.
-intro.elim f
-  [simplify.intro.destruct H
-  |simplify.intro.destruct H
-  |simplify.generalize in match H.
-   cases (numerator f1)
-    [intro.elim H1.reflexivity
-    |simplify.intro.
-     cases z;simplify;intro;destruct H2
-    |simplify.intro.
-     cases z;simplify;intro;destruct H2
-    ]
-  ]
-qed.
-
-theorem numerator_nat_fact_to_fraction: \forall g:nat_fact. 
-numerator (nat_fact_to_fraction g) = nfa_proper g.
-intro.
-elim g
-  [simplify.reflexivity.
-  |simplify.rewrite > H.simplify.
-   cases n;reflexivity
-  ]
-qed.
-
 (* double elimination principles *)
 theorem fraction_elim2:
 \forall R:fraction \to fraction \to Prop.