proposition: Theorem FPredProp : forall x y : float, Fcanonic radix b x -> Fcanonic radix b y -> (x < y)%R -> (x <= FPred y)%R.
proof: Proof. intros x y H' H'0 H'1; rewrite FPredFopFSucc. rewrite <- (Fopp_Fopp x). unfold FtoRradix in |- *; rewrite Fopp_correct with (x := Fopp x). rewrite Fopp_correct with (x := FSucc b radix precision (Fopp y)); auto with real. apply Ropp_le_contravar. apply FSuccProp; auto with zarith. now apply FcanonicFopp. now apply FcanonicFopp. repeat rewrite Fopp_correct; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz