proposition: Lemma existence_representant_angle : forall (A B C : PO) (x : R), distance A B = 1 -> exists D : PO, distance C D = 1 /\ image_angle x = cons_AV (vec A B) (vec C D).
proof: Proof. intros. apply existence_representant_cons; auto. Qed.