proposition: Lemma angle_nul : forall A B : PO, A <> B -> image_angle 0 = cons_AV (vec A B) (vec A B).
proof: Proof. intros. elim existence_representant_unitaire with (A := A) (B := B); [ intros C H0; try clear existence_representant_unitaire; try exact H0 | auto ]. rewrite angles_representants_unitaires; auto. rewrite <- H0. cut (A <> C); intros. cut (image_angle (- pi) = cons_AV (vec C A) (vec A C)); intros. replace 0 with (pi + - pi). rewrite add_mes_compatible; rewrite H2; rewrite (angle_plat (A:=A) (B:=C)); auto. rewrite Chasles; auto. ring. apply mes_oppx; auto. rewrite (angle_plat (A:=A) (B:=C)); auto. elim (def_representant_unitaire2 (A:=A) (B:=B) (C:=C)); auto; intros. elim H2; auto with geo. Qed.