proposition: Lemma coplanaire_ordre_cycle : forall A B C D : PO, coplanaires A B C D -> coplanaires B C D A.
proof: Proof. intros. elim H; clear H; intros; auto with geo. elim coplanaires1_vecteur_def with (A := A) (B := B) (C := C) (D := D); [ intros x H0; elim H0; [ intros y H1; try clear H0 coplanaires1_vecteur_def; try exact H1 ] | auto ]. elim (classic (y = 1 + - x)); intros. rewrite H2 in H1. assert (alignes B C D); auto with geo. apply colineaire_alignes with (1 + - x). VReplace (vec B D) (add_PP (vec B A) (vec A D)). rewrite H1. Ringvec. assert (1 + - x + - y <> 0). contrapose H0. RReplace y (y + 0). rewrite <- H3; ring. apply vecteur_def_coplanaires with (k := / (1 + - x + - y) * - y) (k' := / (1 + - x + - y)). VReplace (vec B D) (add_PP (vec B A) (vec A D)). rewrite H1. Fieldvec (1 + - x + - y). Qed.