proposition: Lemma angle_oppu_oppv : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> cons_AV (vec B A) (vec D C) = cons_AV (vec A B) (vec C D) :>AV.
proof: Proof. intros. replace (cons_AV (vec B A) (vec D C)) with (plus (cons_AV (vec B A) (vec A B)) (plus (cons_AV (vec A B) (vec C D)) (cons_AV (vec C D) (vec D C)))). rewrite <- angle_plat; auto. rewrite <- angle_plat; auto. mesure A B C D. replace (pi + (x + pi)) with (x + deuxpi); try ring; auto. rewrite (mesure_mod_deuxpi (x:=x) (A:=A) (B:=B) (C:=C) (D:=D)); auto. unfold deuxpi in |- *; ring. repeat rewrite Chasles; auto. Qed.