proposition: Lemma egalite_cos_Cos : forall (A B C : PO) (x : R), A <> B -> A <> C -> 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. elim existence_representant_unitaire with (A := A) (B := B); [ intros B' H2; try clear existence_representant_unitaire; try exact H2 | auto ]. elim existence_representant_unitaire with (A := A) (B := C); [ intros C' H3; try clear existence_representant_unitaire; try exact H3 | auto ]. rewrite (trivial_cos_Cos (A:=A) (B:=B') (C:=C') (x:=x)); auto. rewrite H2; rewrite H3; auto. rewrite angles_representants_unitaires; auto. elim def_representant_unitaire2 with (A := A) (B := B) (C := B'); auto; intros. elim H5; auto with geo. elim def_representant_unitaire2 with (A := A) (B := C) (C := C'); auto; intros. elim H5; auto with geo. rewrite H2; rewrite H3; rewrite H1; rewrite angles_representants_unitaires; auto with geo. Qed.