proposition: Lemma avg_half_sub_no_underflow_aux_aux: forall z:Z, (0 < z)%Z -> (ZnearestE (IZR z / 2) < z)%Z.
proof: Proof. intros z H1. case (Zle_lt_or_eq 1 z); [lia|intros H2|intros H2]. apply lt_IZR. apply Rplus_lt_reg_r with (- ((IZR z)/2)). apply Rle_lt_trans with (-(((IZR z) /2) - IZR (ZnearestE (IZR z / 2)))). right; ring. apply Rle_lt_trans with (1:= RRle_abs _). rewrite Rabs_Ropp. apply Rle_lt_trans with (1:=Znearest_half (fun x => negb (Z.even x)) _). apply Rle_lt_trans with (1*/2);[right; ring|idtac]. apply Rlt_le_trans with ((IZR z)*/2);[idtac|right; field]. apply Rmult_lt_compat_r. lra. now apply IZR_lt. rewrite <- H2. unfold Znearest; simpl. replace (Zfloor (1 / 2)) with 0%Z. rewrite Rcompare_Eq. simpl; lia. simpl; field. unfold Rdiv; rewrite Rmult_1_l. apply sym_eq, Zfloor_imp. simpl; lra. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)