proposition: Lemma avg_naive_correct: av = round_flt a.
proof: Proof. Proof with auto with typeclass_instances. case (Rle_or_lt (bpow (prec + emin)) (Rabs (x+y))). intros H. unfold av,a,avg_naive. rewrite round_generic... now apply sym_eq, FLT_round_half. apply FLT_format_half. apply generic_format_round... apply abs_round_ge_generic... apply generic_format_FLT_bpow... unfold Prec_gt_0 in prec_gt_0_; lia. intros H. unfold av, avg_naive. replace (round_flt (x + y)) with (x+y). reflexivity. apply sym_eq, round_generic... apply FLT_format_plus_small... left; assumption. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)