proposition: Theorem FshiftCorrectSym : forall x y : float, x = y :>R -> exists n : nat, (exists m : nat, Fshift n x = Fshift m y).
proof: Proof. intros x y H'. case (Z_le_gt_dec (Fexp x) (Fexp y)); intros H'1. exists 0; exists (Z.abs_nat (Fexp y - Fexp x)). rewrite FshiftO. apply sym_equal. apply FshiftCorrectInv; auto. exists (Z.abs_nat (Fexp x - Fexp y)); exists 0. rewrite FshiftO. apply FshiftCorrectInv; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz