proposition: Theorem Veltkamp_tail: x = hx+tx /\ generic_format beta (FLT_exp emin s) tx.
proof: Proof. Proof with auto with typeclass_instances. assert (precisionNotZero : (1 < prec)%Z) by lia. destruct (format_is_pff_format beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero x) as (fx,(Hfx,Hfx')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia; assumption. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (x*(bpow s+1))) as (fp,(Hfp, (Hfp',Hfp''))). rewrite make_bound_Emin in Hfp''; try assumption. replace (--emin)%Z with emin in Hfp'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (x-p)) as (fq,(Hfq, (Hfq',Hfq''))). rewrite make_bound_Emin in Hfq''; try assumption. replace (--emin)%Z with emin in Hfq'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (q+p)) as (fhx,(Hfhx, (Hfhx',Hfhx''))). rewrite make_bound_Emin in Hfhx''; try assumption. replace (--emin)%Z with emin in Hfhx'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (x-hx)) as (ftx,(Hftx, (Hftx',Hftx''))). rewrite make_bound_Emin in Hftx''; try assumption. replace (--emin)%Z with emin in Hftx'' by lia. destruct Veltkamp_tail with beta (make_bound beta prec emin) (Z.abs_nat s) (Z.abs_nat prec) fx fp fq fhx ftx as (tx', (H1,(H2,(H3,H4)))); try assumption. apply radix_gt_1. apply make_bound_p; lia. replace 2%nat with (Z.abs_nat 2) by easy. apply Zabs_nat_le; lia. apply Nat2Z.inj_le. rewrite inj_abs; lia. rewrite Hfx; rewrite inj_abs; try lia. rewrite bpow_powerRZ in Hfp'; apply Hfp'. rewrite Hfx, Hfp''; apply Hfq'. rewrite Hfp'', Hfq''; apply Hfhx'. rewrite Hfhx'', Hfx; apply Hftx'. split. rewrite <- Hfx, <-H2, Hfhx'', H1, Hftx''; easy. unfold tx; rewrite <- Hftx'', <- H1. replace emin with (-dExp (Bound (Pos.of_succ_nat (Peano.pred (Z.abs_nat (Zpower_nat beta (Z.abs_nat s))))) (dExp (make_bound beta prec emin))))%Z. apply pff_format_is_format; try assumption; try lia. simpl. rewrite Zpos_P_of_succ_nat, inj_pred. rewrite <- Zsucc_pred. apply inj_abs. apply Zpower_NR0. apply Zlt_le_weak; apply radix_gt_0. apply sym_not_eq, Nat.lt_neq, lt_Zlt_inv. rewrite inj_abs. apply Zpower_nat_less. apply radix_gt_1. apply Zpower_NR0. apply Zlt_le_weak; apply radix_gt_0. simpl. rewrite Zabs2N.id_abs. rewrite Z.abs_neq; lia. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat