proposition: Lemma distance_coordonnees : forall (O I J M : PO) (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)) :>PP -> distance O M = sqrt (Rsqr x + Rsqr y) :>R.
proof: Proof. unfold distance in |- *; intros. rewrite (scalaire_coordonnees (O:=O) (I:=I) (J:=J) (M:=M) (N:=M) (x:=x) (y:=y) (x':=x) (y':=y)); eauto. Qed.