proposition: Lemma imageZeroPi_paralelles: forall A B C D: PO, A<>B->C<>D-> (cons_AV(vec A B)(vec C D) = image_angle 0) \/(cons_AV(vec A B)(vec C D) = image_angle pi) -> paralleles (droite A B) (droite C D).
proof: Proof. intros A B C D H H1 H2. set (B' := translation A C B). assert (H3:= refl_equal B'); unfold B' at 2 in H3. assert (H4 : C =translation A C A) by (apply translation_trivial;auto). assert (H5 :vec A B =vec C B') by (apply (@translation_bipoint A C);auto). rewrite H5 in H2. assert (H6:C <>B'). red;intro H7. rewrite H7 in H5. rewrite <-(@mult_1_vec B' B') in H5. rewrite <-vecteur_nul in H5. assert (A = B) by (apply vecteur_nul_conf;auto). elim H;auto. apply (@paralleles_trans A B C B' C D);auto. rewrite <-(@mult_1_vec C B') in H5. apply (colineaires_paralleles (k:=1) );auto . elim H2;intro H7. elim (@angle_nul_positif_colineaire C B' D);auto. intros x [H8 H9]. assert (paralleles (droite C D)(droite C B')) by (apply colineaires_paralleles with (k:=x);auto). apply paralleles_sym;assumption. elim (@angle_pi_negatif_colineaire C B' D);auto. intros x [H8 H9]. assert (paralleles (droite C D)(droite C B')) by (apply colineaires_paralleles with (k:=x);auto). apply paralleles_sym;assumption. Qed.