proposition: Lemma paralleles_sym : forall A B C D : PO, A <> B -> C <> D -> paralleles (droite A B) (droite C D) -> paralleles (droite C D) (droite A B).
proof: Proof. intros A B C D H H1 H0; try assumption. elim def_paralleles2 with (3 := H0); intros; auto. elim (classic (x = 0)); intros. rewrite H3 in H2. absurd (A = B); auto. apply conversion_PP with (a := 1) (b := 1); auto. RingPP1 H2; RingPP; auto with *. auto with *. apply def_paralleles with (k := / x); auto. apply mult_PP_regulier with x; auto. VReplace (mult_PP x (add_PP (cons 1 D) (cons (-1) C))) (add_PP (cons x D) (cons (- x) C)). rewrite <- H2. FieldPP x. Qed.