proposition: Lemma average_symmetry: forall u v, average u v = average v u.
proof: Proof. intros u v; unfold average. case (Rle_bool_spec 0 u); case (Rle_bool_spec 0 v); intros. rewrite 2!Rabs_right; try apply Rle_ge; try assumption. case (Rle_bool_spec u v); case (Rle_bool_spec v u); trivial. intros; replace u with v; trivial; auto with real. intros H1 H2; contradict H1; auto with real. apply avg_naive_symmetry. apply avg_naive_symmetry. rewrite 2!Rabs_left; try assumption. case (Rle_bool_spec (-u) (-v)); case (Rle_bool_spec (-v) (-u)); trivial. intros; replace u with v; trivial; auto with real. intros H1 H2; contradict H1; auto with real. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)