proposition: Theorem the_cube : forall A B C D E F G H I : PO, 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 H51; try assumption. elim H0; intros. elim H1; intros. elim H3; intros. elim H6; intros H7 H8; try clear H6; try exact H8. elim H5; intros H6 H9; try clear H5; try exact H9. elim H4; intros H5 H10; elim H10; intros H11 H12; try clear H10 H4; try exact H12. elim H2; intros H4 H10; try clear H2; try exact H10. elim H4; intros. elim H13; intros H14 H15; elim H15; intros H16 H17; try clear H15 H13; try exact H16. cut (vec A F = add_PP (mult_PP 1 (vec A B)) (mult_PP 1 (vec A E))); intros. 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. apply exercice_cube with (3 := H0); auto. apply distance_non_nulle. replace (vec D F) with (add_PP (mult_PP 1 (vec A F)) (mult_PP (-1) (vec A D))). rewrite scalaire_bilineaire. replace (scalaire (vec A F) (vec A F)) with 2. cut (scalaire (vec A F) (vec A D) = 0); intros. rewrite H20; rewrite H17. rewrite scalaire_sym; rewrite H20. try discrR. rewrite H13. rewrite scalaire_lineaire_g. rewrite H18. rewrite scalaire_sym; rewrite H19. ring. rewrite H13. rewrite scalaire_bilineaire. rewrite H15; rewrite H10; rewrite H16. rewrite scalaire_sym; rewrite H15. ring. Ringvec. cut (vec E B = add_PP (mult_PP 1 (vec A B)) (mult_PP (-1) (vec A E))); intros. cut (vec E G = add_PP (mult_PP 1 (vec A B)) (mult_PP 1 (vec A D))); intros. apply equilateral_non_alignes; auto. apply distance_non_nulle. rewrite H20. rewrite scalaire_bilineaire. rewrite H15; rewrite H10; rewrite H16. rewrite scalaire_sym; rewrite H15. try discrR. rewrite H20. rewrite scalaire_bilineaire. rewrite H21. rewrite scalaire_bilineaire. rewrite H15; rewrite H10; rewrite H16. rewrite scalaire_sym; rewrite H15. rewrite H17; rewrite H18. rewrite scalaire_sym; rewrite H18. ring. replace (vec B G) with (add_PP (mult_PP 1 (vec E G)) (mult_PP (-1) (vec E B))). rewrite scalaire_bilineaire. rewrite H20. rewrite scalaire_bilineaire. rewrite H21. repeat rewrite scalaire_bilineaire. rewrite H15; rewrite H10; rewrite H16. rewrite scalaire_sym; rewrite H15. rewrite H17; rewrite H18. rewrite scalaire_sym; rewrite H18. rewrite H19; rewrite scalaire_sym; rewrite H19. ring. Ringvec. rewrite <- H8. rewrite H6; rewrite H9. Ringvec. Ringvec. apply def_orthogonal; auto. apply def_orthogonal; auto. apply def_orthogonal; auto. rewrite H6; rewrite H9; rewrite H7. Ringvec. Qed.