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