proposition: Lemma angle_droites_paralleles : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> paralleles (droite C D) (droite A B) -> double_AV (cons_AV (vec A B) (vec C D)) = image_angle 0.
proof: Proof. intros. elim paralleles_vecteur with (A := C) (B := D) (C := A) (D := B); [ intros k H3; try clear paralleles_vecteur; auto | auto | auto | auto ]. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := k); intros E H4; try clear existence_representant_mult_vecteur; try exact H4. cut (vec C D = vec A E); intros. rewrite H2. cut (alignes A B E); intros. apply angle_alignes with (3 := H5); auto. unfold not in |- *; intros; apply H0. apply conversion_PP with (a := 1) (b := 1); auto with real. RingPP2 H2. rewrite H6. Ringvec. apply colineaire_alignes with k; auto. rewrite H4; auto. Qed.