proposition: Lemma Dcompare_correct : forall x : float2, forall y : float10, Dcompare x y = Rcompare x y.
proof: Proof. assert (forall e, Zpower_pos 5 e * Zpower_pos 2 e = Zpower_pos 10 e)%Z. intros e. rewrite 3!Zpower_pos_nat. induction (nat_of_P e). apply refl_equal. change ((5 * Zpower_nat 5 n) * (2 * Zpower_nat 2 n) = 10 * Zpower_nat 10 n)%Z. rewrite <- IHn. ring. intros x (ym, ye). unfold Dcompare, float10R. simpl. destruct ye as [|ye|ye] ; rewrite Fcomp2_correct. apply refl_equal. apply f_equal. unfold float2R, F2R. simpl. rewrite mult_IZR, Rmult_assoc, <- mult_IZR. now apply (f_equal (fun v => IZR ym * IZR v)%R). unfold float2R at 1, F2R at 1. simpl. replace (IZR (Fnum x * Zpower_pos 5 ye) * bpow radix2 (Fexp x))%R with (x * IZR (Zpower_pos 5 ye))%R. rewrite <- (Rcompare_mult_r (IZR (Zpower_pos 2 ye))). rewrite Rmult_assoc, <- mult_IZR, H. rewrite <- (Rcompare_mult_r (IZR (Zpower_pos 10 ye)) x). apply f_equal. unfold float2R, F2R. simpl. rewrite 2!Rmult_assoc, 2!Rinv_l. apply refl_equal. apply Rgt_not_eq. exact (bpow_gt_0 radix10 (Zpos ye)). apply Rgt_not_eq. exact (bpow_gt_0 radix2 (Zpos ye)). exact (bpow_gt_0 radix10 (Zpos ye)). exact (bpow_gt_0 radix2 (Zpos ye)). unfold float2R, F2R. simpl. rewrite mult_IZR. ring. Qed.
imports: Flocq.Core.Defs Gappa_common