proposition: Lemma coordonnees_scalaire_base : forall O I J M : PO, repere_orthonormal O I J -> vec O M = add_PP (mult_PP (scalaire (vec O M) (vec O I)) (vec O I)) (mult_PP (scalaire (vec O M) (vec O J)) (vec O J)).
proof: Proof. intros. elim existence_coordonnees with (O := O) (I := I) (J := J) (M := M); [ intros x H1; elim H1; intros y H2; try clear H1; try exact H2 | auto with geo ]. elim H; intros H1 H11; elim H11; intros H3 H4; try clear H11; try exact H4. cut (x = scalaire (vec O M) (vec O I) /\ y = scalaire (vec O M) (vec O J)); intros. elim H0; intros H6 H7; try clear H5; try exact H7. rewrite <- H7; rewrite <- H6; auto. rewrite H2. split; [ try assumption | idtac ]. Simplscal. rewrite H3; rewrite scalaire_sym; rewrite H1; ring. Simplscal. rewrite H4; rewrite H1; ring. Qed.