Even more Q stuff moved around.

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

diff --git a/helm/software/matita/library/Q/fraction/fraction.ma b/helm/software/matita/library/Q/fraction/fraction.ma
index 81b60de91fc924a0e3d10214d920c00fb461b123..ba4b417f6c2b6d067b2e1c331eaa8e87ee60e12f 100644 (file)
--- 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.