proposition: Lemma vec_directeur_permute : forall A B C D : PO, A <> B -> C <> D -> vec_directeur (vec A B) (droite C D) -> vec_directeur (vec C D) (droite A B).
proof: Proof. intros. apply vec_directeur_def2; auto. rewrite determinant_antisymetrique. rewrite vec_directeur_def; auto. ring. Qed.