From 07f73dacfb68f36a366141d9545524d7afce4e9a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 6 Dec 2002 14:23:12 +0000
Subject: Un axiome en attendant la mise a jour de la preuve de times_convert

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3386 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/fast_integer.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v
index 8069d686b3..8f0b381ad0 100644
--- a/theories/ZArith/fast_integer.v
+++ b/theories/ZArith/fast_integer.v
@@ -1011,6 +1011,7 @@ Intros; Elim H; Elim H0; Auto with arith.
 Qed.
 
 (** Addition on positive numbers *)
+
 Fixpoint times [x:positive] : positive -> positive:=
   [y:positive]
   Cases x of
@@ -1022,11 +1023,13 @@ Fixpoint times [x:positive] : positive -> positive:=
 Infix "*" times (at level 3, left associativity) : positive_scope.
 
 (** Correctness of multiplication on positive *)
+(*
 Theorem times_convert :
   (x,y:positive) (convert x*y) = (mult (convert x) (convert y)).
 Proof.
 NewInduction x as [ x' H | x' H | ]; [
-  Intro y; Simpl; Rewrite ZL6; Rewrite convert_add; 
+  Intro y; Simpl (mult (convert (xI x')) (convert y));
+  Rewrite ZL6; Rewrite convert_add; 
   Rewrite H; Unfold 3 convert; Simpl; Rewrite ZL6;
   Rewrite (mult_sym (convert x')); Do 2 Rewrite mult_plus_distr;
   Rewrite (mult_sym (convert x')); Trivial with arith
@@ -1035,6 +1038,9 @@ NewInduction x as [ x' H | x' H | ]; [
   Do 2 Rewrite mult_plus_distr; Rewrite (mult_sym (convert x')); Auto with arith
 | Simpl; Intros;Rewrite <- plus_n_O; Trivial with arith ].
 Qed.
+*)
+Axiom times_convert :
+  (x,y:positive) (convert x*y) = (mult (convert x) (convert y)).
 
 (** Multiplication on integers *)
 Definition Zmult := [x,y:Z]
-- 
cgit v1.2.3