proposition: Theorem FSuccNegCanonic : forall a : float, (a <= 0)%R -> Fcanonic radix b a -> Fcanonic radix b (FSucc a).
proof: Proof. intros a H' H'0; case H'0; intros H'1. case (floatDec a (Float (- nNormMin radix precision) (- dExp b))); intros H'2. rewrite H'2; right; apply FSuccNormNegNormMin; auto. left; apply FSuccNormNegNotNormMin; auto. apply FSuccSubnormal; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz