proposition: Theorem FcanonicFabs : forall p : float, Fcanonic p -> Fcanonic (Fabs p).
proof: Proof. intros p H'; case H'; clear H'. intros H; left. apply FnormalFabs; auto. intros H; right. apply FsubnormFabs; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz