proposition: Lemma rectangle_Pythagore : forall A B C : PO, orthogonal (vec A B) (vec A C) <-> scalaire (vec B C) (vec B C) = scalaire (vec A B) (vec A B) + scalaire (vec A C) (vec A C) :>R.
proof: Proof. intros. generalize (triangle_Pythagore A B C); unfold iff in |- *; intros. elim H; intros H0 H1; try clear H; try exact H0. split; [ intros H; try assumption | idtac ]. apply H0; auto with geo. intros H; try assumption. apply def_orthogonal2; auto. Qed.