proposition: Theorem FPredCanonic : forall a : float, Fcanonic radix b a -> Fcanonic radix b (FPred a).
proof: Proof. intros a H'. rewrite FPredFopFSucc. apply FcanonicFopp. apply FSuccCanonic; try easy. now apply FcanonicFopp. Qed.
imports: Reals ZArith List PeanoNat Psatz