proposition: Lemma permute_angles : forall A B C D E F G I : PO, A <> B :>PO -> C <> D :>PO -> E <> F :>PO -> G <> I :>PO -> cons_AV (vec A B) (vec C D) = cons_AV (vec E F) (vec G I) :>AV -> cons_AV (vec C D) (vec A B) = cons_AV (vec G I) (vec E F) :>AV.
proof: Proof. intros A B C D E F G I H H0 H1 H2 H3; try assumption. rewrite <- def_opp; auto. rewrite <- (def_opp (A:=E) (B:=F) (C:=G) (D:=I)); auto. rewrite <- H3; auto. Qed.