proposition: Lemma composantes_projete_orthogonal : forall (a b : R) (M H : PO), H = projete_orthogonal O I M -> vec O M = add_PP (mult_PP a (vec O I)) (mult_PP b (vec O J)) -> vec O H = mult_PP a (vec O I).
proof: Proof. intros. elim def_projete_orthogonal2 with (A := O) (B := I) (C := M) (H := H); [ intros | auto with geo | auto ]. halignes H2 k. absurd (O = I); auto with geo. cut (vec H M = add_PP (mult_PP (a + - k) (vec O I)) (mult_PP b (vec O J))); intros. cut (scalaire (vec O I) (vec H M) = a + - k); intros. replace a with k; auto. replace a with (k + (a + - k)); [ idtac | ring ]. cut (scalaire (vec O I) (vec H M) = 0); intros; auto with geo. rewrite <- H6; rewrite H7; ring. elim existence_representant_vecteur with (A := O) (B := H) (C := M); intros D H6; try clear existence_representant_vecteur; rewrite <- H6. rewrite (scalaire_coordonnees (O:=O) (I:=I) (J:=J) (M:=I) (N:=D) (x:=1) (y:=0) (x':=a + - k) (y':=b)); auto with geo. ring. Ringvec. rewrite H6; auto with geo. replace (vec H M) with (add_PP (vec O M) (mult_PP (-1) (vec O H))); [ idtac | Ringvec ]. rewrite H1; rewrite H4; Ringvec. Qed.