proposition: Lemma mes_opp_opp : forall (A B C D E F G I : PO) (a b : R), A <> B -> C <> D -> E <> F -> G <> I -> image_angle a = cons_AV (vec A B) (vec C D) -> image_angle b = cons_AV (vec E F) (vec G I) -> image_angle b = image_angle (- a) -> cons_AV (vec E F) (vec G I) = opp (cons_AV (vec A B) (vec C D)).
proof: Proof. intros A B C D E F G I a b H H0 H1 H2 H3 H4 H5; try assumption. rewrite <- H4; rewrite def_opp; auto. rewrite <- (mes_oppx (A:=A) (B:=B) (C:=C) (D:=D) (x:=a)); auto. Qed.