proposition: Lemma diagonales_carre : forall A B C D : PO, carre A B C D -> orthogonal (vec A C) (vec D B).
proof: Proof. intros. elim H; clear H; intros. apply def_orthogonal2. elim H0; intros H2 H3; elim H3; intros H4 H5; try clear H3 H0; try exact H5. cut (scalaire (vec A B) (vec A D) = 0); intros. replace (vec A C) with (add_PP (mult_PP 1 (vec A B)) (mult_PP 1 (vec A D))). replace (vec D B) with (add_PP (mult_PP (-1) (vec A D)) (mult_PP 1 (vec A B))). rewrite scalaire_bilineaire. rewrite H4; rewrite H5; rewrite H0. rewrite scalaire_sym; rewrite H0; ring. Ringvec. rewrite H. Ringvec. apply def_orthogonal; auto. Qed.