proposition: Lemma coplanaire_ordre_permute : forall A B C D : PO, coplanaires A B C D -> coplanaires A B D C.
proof: Proof. intros. elim H; clear H; intros; auto with geo. elim (coplanaires1_vecteur_def H); intros. elim H0; [ intros y H1; try clear H0; try exact H1 ]. elim (classic (y = 0)); intros. assert (alignes A B D); auto with geo. apply colineaire_alignes with x. rewrite H1; rewrite H0; Ringvec. apply vecteur_def_coplanaires with (k := / y * - x) (k' := / y). rewrite H1. Fieldvec y. Qed.