proposition: Lemma exercice : forall A B C D E F G H I : PO, D <> F -> ~ alignes E B G -> parallelepipede A B C D E F G H -> I = centre_gravite E B G -> coplanaires E B G I /\ alignes F D I.
proof: Proof. intros A B C D E F G H I H20 H0 H1 H51; try assumption. rewrite H51. split; [ auto with geo | idtac ]. cut (vec F G = vec A D). intros H10. unfold parallelepipede in H1. elim H1; intros H2 H3; elim H2; intros H4 H5; try clear H2 H1; try exact H4. elim H3; intros H2 H12; try clear H3. cut (vec F D = mult_PP 3 (vec F (centre_gravite E B G))); intros. cut (3 <> 0); intros; auto with real. apply colineaire_alignes with (/ 3); auto. rewrite H1. Fieldvec 3; auto. cut (add_PP (mult_PP 3 (vec (centre_gravite E B G) F)) (vec F D) = zero); intros. VReplace (vec F D) (add_PP (vec F D) (mult_PP (-1) zero)). rewrite <- H1. Ringvec. VReplace (vec F D) (add_PP (vec F B) (add_PP (vec B A) (vec A D))). replace (vec B A) with (vec F E); auto. replace (vec A D) with (vec F G); auto. VReplace (add_PP (vec F B) (add_PP (vec F E) (vec F G))) (add_PP (vec F E) (add_PP (vec F B) (vec F G))). replace (add_PP (vec F E) (add_PP (vec F B) (vec F G))) with (mult_PP 3 (vec F (barycentre (cons 1 E) (cons 2 (barycentre (cons 1 B) (cons 1 G)))))); auto. unfold vec, centre_gravite, milieu in |- *; RingPP. VReplace (add_PP (vec F B) (vec F G)) (add_PP (mult_PP 1 (vec F B)) (mult_PP 1 (vec F G))). rewrite (prop_vecteur_bary (a:=1) (b:=1) (A:=B) (B:=G) (G:=barycentre (cons 1 B) (cons 1 G)) F); auto. VReplace (vec F E) (mult_PP 1 (vec F E)). replace (1 + 1) with 2 by ring. rewrite (prop_vecteur_bary (a:=1) (b:=2) (A:=E) (B:=barycentre (cons 1 B) (cons 1 G)) (G:=barycentre (cons 1 E) (cons 2 (barycentre (cons 1 B) (cons 1 G)))) F) ; auto. discrR. discrR. cut (vec A B = vec E F); intros; auto. VReplace (vec B A) (mult_PP (-1) (vec A B)). rewrite H1. Ringvec. rewrite H4. rewrite H5; auto. apply parallelepipede_parallelogramme with (1 := H1). Qed.