proposition: Lemma triangle_Pythagore : forall A B C : PO, scalaire (vec A B) (vec A C) = 0 <-> 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; red in |- *. rewrite (difference_Pythagore A B C). split; [ intros H; try assumption | idtac ]. rewrite H. ring. intros H; try assumption. cut (2 * scalaire (vec A B) (vec A C) = 0); intros. elim Rmult_integral with (r1 := 2) (r2 := scalaire (vec A B) (vec A C)); [ intros H1; try clear without_div_Od | intros H1; try clear without_div_Od; try exact H1 | try assumption ]. absurd (2 = 0); try assumption. discrR. replace 0 with (scalaire (vec A B) (vec A B) + scalaire (vec A C) (vec A C) + -1 * (scalaire (vec A B) (vec A B) + scalaire (vec A C) (vec A C))). pattern (scalaire (vec A B) (vec A B) + scalaire (vec A C) (vec A C)) at 2 in |- *. rewrite <- H. ring. ring. Qed.