proposition: Lemma opp_angle : forall a b : AV, plus a b = image_angle 0 :>AV -> b = opp a :>AV.
proof: Proof. intros. mes a. mes b. replace (image_angle (- x)) with (plus (image_angle (- x)) (image_angle 0)); auto with geo. rewrite <- H. rewrite H1; rewrite H0. repeat rewrite <- add_mes_compatible. pattern x0 at 1 in |- *. replace x0 with (- x + (x + x0)); auto. ring. Qed.