proposition: Lemma affixe_projete_orthogonal : forall (z : C) (a b : R) (M H : PO), H = projete_orthogonal O I M -> z = affixe M -> z = cons_cart a b -> Rinj a = affixe H.
proof: Proof. unfold Rinj in |- *; intros. cut (vec O H = mult_PP a (vec O I)); intros. symmetry in |- *. apply (cart_point_complexe (z:=affixe H) (a:=a) (b:=0) (M:=H)); auto. rewrite H3; Ringvec. apply (composantes_projete_orthogonal (a:=a) (b:=b) (M:=M) (H:=H)); auto. eauto with geo. Qed.