proposition: Lemma exercice_cube : forall A B C D E F G H I : PO, D <> F -> ~ alignes E B G -> cube A B C D E F G H -> I = centre_gravite E B G -> alignes F D I /\ orthogonaux (droite F D) (plan E B G).
proof: Proof. intros A B C D E F G H I H0 H1 H2 H51; try assumption. elim H2; intros; clear H2. elim H3; intros; clear H3. elim H5; intros H3 H6; elim H6; intros H7 H8; try clear H6 H5; try exact H8. elim H4; intros H5 H6; try clear H4; try exact H6. split; [ try assumption | idtac ]. elim exercice with (A := A) (B := B) (C := C) (D := D) (E := E) (F := F) (G := G) (H := H) (I := I); [ try clear exercice; auto | auto | auto | auto | auto ]. elim H5; intros; clear H5. elim H9; intros H5 H10; elim H10; intros H11 H12; try clear H10 H9; try exact H12. elim H2; intros. elim H10; intros H13 H14; try clear H10; try exact H14. elim H9; intros H10 H15; try clear H9; try exact H15. cut (scalaire (vec A B) (vec A E) = 0); intros. cut (scalaire (vec A B) (vec A D) = 0); intros. cut (scalaire (vec A D) (vec A E) = 0); intros. cut (E <> B); intros. cut (E <> G); intros. cut (vec F D = add_PP (vec F A) (vec A D)); intros. apply def_orthogonaux; auto. apply def_orthogonales; auto. apply def_orthogonal2. rewrite scalaire_sym. rewrite H20. rewrite scalaire_somme_g. replace (scalaire (vec F A) (vec E B)) with 0. replace (scalaire (vec A D) (vec E B)) with 0. ring. replace (vec E B) with (add_PP (mult_PP (-1) (vec A E)) (mult_PP 1 (vec A B))). rewrite scalaire_lineaire_d. rewrite H17. rewrite scalaire_sym. rewrite H16. ring. Ringvec. replace (vec E B) with (add_PP (mult_PP (-1) (vec A E)) (mult_PP 1 (vec A B))). replace (vec F A) with (add_PP (mult_PP (-1) (vec A E)) (mult_PP (-1) (vec A B))). rewrite scalaire_bilineaire. rewrite H11; rewrite H6; rewrite H9. rewrite scalaire_sym. rewrite H9. ring. rewrite H10; rewrite H15; rewrite H13. Ringvec. Ringvec. apply def_orthogonales; auto. apply def_orthogonal2. replace (vec E G) with (add_PP (vec A B) (vec A D)). rewrite scalaire_somme_g. rewrite scalaire_sym. rewrite (scalaire_sym A D F D). rewrite H20. rewrite scalaire_somme_g. rewrite scalaire_somme_g. rewrite H12. rewrite (scalaire_sym A D A B). rewrite H16. replace (vec F A) with (add_PP (mult_PP (-1) (vec A E)) (mult_PP (-1) (vec A B))). rewrite scalaire_lineaire_g. rewrite scalaire_lineaire_g. rewrite H11; rewrite H16. rewrite scalaire_sym. rewrite H9. rewrite scalaire_sym. rewrite H17. ring. rewrite H10; rewrite H15; rewrite H13. Ringvec. replace (vec E G) with (add_PP (vec E F) (vec F G)). rewrite H10; rewrite H15; rewrite H13. rewrite parallelepipede_parallelogramme with (1 := H2); auto. Ringvec. Ringvec. apply distance_non_nulle. replace (vec E G) with (add_PP (mult_PP 1 (vec A B)) (mult_PP 1 (vec A D))). rewrite scalaire_bilineaire. rewrite H11; rewrite H12; rewrite H16. rewrite scalaire_sym; rewrite H16. replace (1 * 1 * 1 + 1 * 1 * 0 + (1 * 1 * 0 + 1 * 1 * 1)) with 2. discrR. ring. replace (vec E G) with (add_PP (vec E F) (vec F G)). rewrite H10; rewrite H15; rewrite H13. rewrite parallelepipede_parallelogramme with (1 := H2); auto. Ringvec. Ringvec. apply distance_non_nulle. replace (vec E B) with (add_PP (mult_PP (-1) (vec A E)) (mult_PP 1 (vec A B))). rewrite scalaire_bilineaire. rewrite H11; rewrite H9; rewrite H6. rewrite scalaire_sym; rewrite H9. replace (-1 * -1 * 1 + -1 * 1 * 0 + (1 * -1 * 0 + 1 * 1 * 1)) with 2. discrR. ring. Ringvec. apply def_orthogonal; auto. apply def_orthogonal; auto. apply def_orthogonal; auto. Qed.