proposition: Lemma trivial_cos_Cos : forall (A B C : PO) (x : R), distance A B = 1 -> distance A C = 1 -> image_angle x = cons_AV (vec A B) (vec A C) -> cos x = Cos (cons_AV (vec A B) (vec A C)).
proof: Proof. intros. rewrite (def_cos (A:=A) (B:=B) (C:=C) (x:=x)); auto. rewrite (def_Cos (A:=A) (B:=B) (C:=C)); auto. Qed.