proposition: Lemma concours_sym : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> concours (droite A B) (droite C D) -> concours (droite C D) (droite A B).
proof: Proof. intros A B C D H10 H11 H; try assumption. elim def_concours2 with (3 := H); auto; intros. apply def_concours with x; auto. elim H0; intros H1 H2; try clear H0; try exact H2. elim H0; intros H1 H2; try clear H0; try exact H1. Qed.