proposition: Theorem FcanonicFopp : forall p : float, Fcanonic p -> Fcanonic (Fopp p).
proof: Proof. intros p H'; case H'; intros H'1. left; apply FnormalFop; auto. right; apply FsubnormFopp; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz