proposition: Lemma angle_argument : forall (z z' : C) (M M' : PO), O <> M :>PO -> O <> M' :>PO -> z = affixe M :>C -> z' = affixe M' :>C -> cons_AV (vec O M) (vec O M') = plus (argument z') (opp (argument z)) :>AV.
proof: Proof. intros. rewrite (argument_def2 (M:=M) (z:=z)); auto. rewrite (argument_def2 (M:=M') (z:=z')); auto. rewrite Chasles_diff; auto with geo. Qed.