proposition: Theorem FSuccProp : forall x y : float, Fcanonic radix b x -> Fcanonic radix b y -> (x < y)%R -> (FSucc x <= y)%R.
proof: Proof. intros x y H' H'0 H'1; case (Rle_or_lt 0 x); intros H'2. apply FSuccPropPos; auto. apply FSuccPropNeg; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz