proposition: Lemma coplanaire_trans : forall A B C D E : PO, ~ alignes A B C -> coplanaires A B C D -> coplanaires A B C E -> coplanaires B C D E.
proof: Proof. intros. elim H1; clear H1; intros. tauto. elim H0; clear H0; intros. tauto. elim coplanaires1_vecteur_def with (A := A) (B := B) (C := C) (D := D); [ intros x H2; elim H2; [ intros y H3; try clear H2; try exact H3 ] | auto ]. elim coplanaires1_vecteur_def with (A := A) (B := B) (C := C) (D := E); [ intros k H4; elim H4; [ intros k' H5; try clear H4; try exact H5 ] | auto ]. elim (classic (y = 1 + - x)); intros. rewrite H2 in H3. 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 H3. Ringvec. assert (1 + - x + - y <> 0). contrapose H0. RReplace y (y + 0). rewrite <- H4; ring. assert (vec B A = add_PP (mult_PP (/ (1 + - x + - y) * - y) (vec B C)) (mult_PP (/ (1 + - x + - y)) (vec B D))). VReplace (vec B D) (add_PP (vec B A) (vec A D)). rewrite H3. Fieldvec (1 + - x + - y). assert (vec B E = add_PP (mult_PP (1 + - k + - k') (vec B A)) (mult_PP k' (vec B C))). VReplace (vec B E) (add_PP (vec B A) (vec A E)). rewrite H5. Ringvec. apply vecteur_def_coplanaires with (k := k' + / (1 + - x + - y) * - y * (1 + - k + - k')) (k' := / (1 + - x + - y) * (1 + - k + - k')). rewrite H7; rewrite H6. Fieldvec (1 + - x + - y). Qed.