proposition: Lemma scalaire_coordonnees : forall (O I J M N : PO) (x y x' y' : R), repere_orthonormal O I J -> vec O M = add_PP (mult_PP x (vec O I)) (mult_PP y (vec O J)) -> vec O N = add_PP (mult_PP x' (vec O I)) (mult_PP y' (vec O J)) -> scalaire (vec O M) (vec O N) = x * x' + y * y'.
proof: Proof. unfold repere_orthonormal in |- *; intros. rewrite H0; rewrite H1. Simplscal. elim H; intros H4 H5; elim H5; intros H6 H7; try clear H5 H; try exact H7. rewrite H7; rewrite H6; rewrite H4; rewrite scalaire_sym; rewrite H4; ring. Qed.