proposition: Theorem FSuccCanonic : forall a : float, Fcanonic radix b a -> Fcanonic radix b (FSucc a).
proof: Proof. intros a H'. case (Rle_or_lt 0 a); intros H'3. apply FSuccPosNotMax; auto. apply FSuccNegCanonic; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz