proposition: Lemma average_zero: a = 0 -> av = 0.
proof: Proof. Proof with auto with typeclass_instances. unfold av,a,average. case (Rle_bool_spec 0 x); case (Rle_bool_spec 0 y); intros. case (Rle_bool_spec (Rabs x) (Rabs y)); intros. apply avg_half_sub_zero... apply avg_half_sub_zero... now rewrite Rplus_comm. apply avg_naive_zero... apply avg_naive_zero... case (Rle_bool_spec (Rabs x) (Rabs y)); intros. apply avg_half_sub_zero... apply avg_half_sub_zero... now rewrite Rplus_comm. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)