proposition: Theorem FdigitEq : forall x y : float, ~ is_Fzero x -> x = y :>R -> Fdigit x = Fdigit y -> x = y.
proof: Proof. intros x y H' H'0 H'1. cut (~ is_Fzero y); [ intros NZy | idtac ]. 2: red in |- *; intros H'2; case H'. 2: apply is_Fzero_rep2; rewrite H'0; apply is_Fzero_rep1; auto. case (Zle_or_lt (Fexp x) (Fexp y)); intros Eq1. case (Zle_lt_or_eq _ _ Eq1); clear Eq1; intros Eq1. absurd (Fdigit (Fshift (Z.abs_nat (Fexp y - Fexp x)) y) = Fdigit y + Z.abs_nat (Fexp y - Fexp x)). rewrite FshiftCorrectInv; auto. rewrite <- H'1. red in |- *; intros H'2. lia. apply Zlt_le_weak; auto. apply FshiftFdigit; auto. apply sameExpEq; auto. absurd (Fdigit (Fshift (Z.abs_nat (Fexp x - Fexp y)) x) = Fdigit x + Z.abs_nat (Fexp x - Fexp y)). rewrite FshiftCorrectInv; auto. rewrite <- H'1. red in |- *; intros H'2. lia. apply Zlt_le_weak; auto. apply FshiftFdigit; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz