proposition: Theorem FinductNeg : 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 q : float, Fcanonic radix b q -> (0 <= q)%R -> (q <= p)%R -> P q.
proof: Proof. intros P p H' H'0 H'1 H'2 q H'3 H'4 H'5. apply FinductNegAux with (p := p) (x := (Fweight p - Fweight q)%Z); auto. cut (Fweight q <= Fweight p)%Z; [ auto with zarith | idtac ]. apply FweightZle; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz