proposition: Lemma angle_vecteurs_arguments : forall (A B A' B' : PO) (z z' : C), A <> B -> A' <> B' -> z = affixe_vec (vec A B) -> z' = affixe_vec (vec A' B') -> cons_AV (vec A B) (vec A' B') = plus (argument z') (opp (argument z)).
proof: Proof. intros A B A' B' z z'; try assumption. elim existence_representant_vecteur with (A := O) (B := A) (C := B); intros M; intros H1. elim existence_representant_vecteur with (A := O) (B := A') (C := B'); intros M'; intros H2. rewrite <- H2; rewrite <- H1; intros. apply angle_argument; auto with geo. apply distinct_egalite_vecteur with (2 := H1); auto. apply distinct_egalite_vecteur with (2 := H2); auto. Qed.