proposition: Theorem FinductNegAux : forall (P : float -> Prop) (p : float), (0 <= p)%R -> Fcanonic radix b p -> P p -> (forall q : float, Fcanonic radix b q -> (0 < q)%R -> (q <= p)%R -> P q -> P (FPred b radix precision q)) -> forall x : Z, (0 <= x)%Z -> forall q : float, x = (Fweight p - Fweight q)%Z -> Fcanonic radix b q -> (0 <= q)%R -> (q <= p)%R -> P q.
proof: Proof. intros P p H' H'0 H'1 H'2 x H'3; pattern x in |- *. apply Z_lt_induction; auto. intros x0 H'4 q H'5 H'6 H'7 H'8. Casec H'8; intros H'8. cut (FSucc b radix precision q <= p)%R; [ intros Rle1 | idtac ]. cut (P (FSucc b radix precision q)); [ intros P1 | idtac ]. rewrite <- (FPredSuc b radix precision) with (x := q); auto with arith. apply H'2; auto with zarith arith. apply FSuccCanonic; auto with zarith. apply Rle_lt_trans with (FtoRradix q); auto. apply (FSuccLt b radix); auto with arith. apply H'4 with (y := (Fweight p - Fweight (FSucc b radix precision q))%Z); auto. split. cut (Fweight (FSucc b radix precision q) <= Fweight p)%Z; auto with zarith. apply FweightZle; auto. apply FSuccCanonic; auto with arith. apply Rle_trans with (FtoRradix q); auto; apply Rlt_le. apply (FSuccLt b radix); auto with arith. rewrite H'5. cut (Fweight q < Fweight (FSucc b radix precision q))%Z; [ auto with zarith | idtac ]. apply FweightLt; auto with zarith. apply FSuccCanonic; auto with arith. apply (FSuccLt b radix); auto with arith. apply FSuccCanonic; auto with arith. apply Rle_trans with (FtoRradix q); auto; apply Rlt_le. apply (FSuccLt b radix); auto with arith. apply (FSuccProp b radix); auto with arith. rewrite <- (FcanonicUnique _ radixMoreThanOne b precision) with (p := p) (q := q); auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz