proposition: Theorem FshiftCorrectInv : forall x y : float, x = y :>R -> (Fexp x <= Fexp y)%Z -> Fshift (Z.abs_nat (Fexp y - Fexp x)) y = x.
proof: Proof. intros x y H' H'0; try apply sameExpEq; auto. apply trans_eq with (y := FtoR y); auto. apply FshiftCorrect. generalize H' H'0; case x; case y; simpl in |- *; clear H' H'0 x y. intros Fnum1 Fexp1 Fnum2 Fexp2 H' H'0; rewrite inj_abs; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz