proposition: Lemma angle_alignes : forall A B C : PO, A <> B :>PO -> A <> C :>PO -> alignes A B C -> double_AV (cons_AV (vec A B) (vec A C)) = image_angle 0.
proof: Proof. intros A B C H H0 H1; unfold double_AV in |- *. rewrite angles_representants_unitaires; auto. elim alignes_representant_unitaire with (A := A) (B := B) (C := C); [ intros; try clear alignes_representant_unitaire; auto | intros; auto | auto | auto | auto ]. rewrite H2. rewrite <- angles_representants_unitaires; auto. rewrite <- angle_nul; auto. rewrite <- add_mes_compatible. replace (0 + 0) with 0; try ring; auto. elim existence_representant_unitaire with (A := A) (B := B); [ intros; try clear existence_representant_unitaire | auto ]. rewrite <- H3. replace (representant_unitaire (vec A C)) with (vec x A). cut (A <> x); intros. rewrite <- angle_plat; auto. rewrite <- add_mes_compatible. replace (pi + pi) with deuxpi; auto. rewrite pi_plus_pi; auto. apply distance_non_nulle. elim def_representant_unitaire2 with (A := A) (B := B) (C := x); [ intros; elim H5; intros H22 H23; rewrite H22; try discrR | auto | auto ]. rewrite H2; rewrite <- H3. Ringvec. Qed.