proposition: Lemma angles_representants_unitaires2 : forall A B C D E F : PO, A <> B -> C <> D -> cons_AV (vec A B) (vec C D) = cons_AV (representant_unitaire (vec A B)) (vec C D).
proof: Proof. intros A B C D E F H H0. assert (H1: cons_AV (vec A B)(vec C D) = cons_AV (representant_unitaire (vec A B))(representant_unitaire(vec C D))). apply angles_representants_unitaires ;auto. rewrite H1. destruct (@existence_representant_unitaire C D H0) as [D' H2]. assert (H3 : exists k:R, k>0 /\ vec C D = mult_PP k (vec C D')). apply (@egalite_representant_unitaire C D' D);auto. destruct (@def_representant_unitaire2 C D D' H0 H2) as [_ [H3 _]]. apply unitaire_distincts ;auto. rewrite H2;apply representant_unitaire_bis;auto. destruct H3 as [k[H3 H4]]. rewrite <-H2. destruct (@existence_representant_unitaire A B H) as [B' H5]. rewrite <-H5. rewrite H4. symmetry. apply angle_produit_positif_r2;auto. destruct (@def_representant_unitaire2 C D D' H0 H2) as [_ [H6 _]]. apply unitaire_distincts ;auto. destruct (@def_representant_unitaire2 A B B' H H5) as [_ [H6 _]]. apply unitaire_distincts ;auto. Qed.