proposition: Theorem produit_vecteur_image : forall (k : R) (z z' : C) (A B A' B' : PO), z = affixe_vec (vec A B) :>C -> z' = affixe_vec (vec A' B') :>C -> vec A' B' = mult_PP k (vec A B) :>PP -> z' = Cmult (Rinj k) z :>C.
proof: Proof. intros. cut (module z' = Rabs k * module z); intros. 2: apply (module_affixe_produit_vecteur (k:=k) (A:=A) (B:=B) (A':=A') (B':=B') (z:=z) (z':=z')); auto. discrimine A B. rewrite (egalite_point_zeroC (z:=z) (A:=A) (B:=B)); auto with geo. rewrite (egalite_point_zeroC (z:=z') (A:=A') (B:=B')); auto with geo. apply vecteur_nul_conf. rewrite H1; rewrite H3; Ringvec. elim (classic (k = 0)); intros. rewrite (egalite_point_zeroC (z:=z') (A:=A') (B:=B')); auto with geo. rewrite H4; rewrite Rinj_zero; ring. apply vecteur_nul_conf. rewrite H1; rewrite H4; Ringvec. cut (A' <> B'); intros. cut (k > 0 \/ k < 0); intros. elim H6; [ intros H7; try clear H6 | intros H7; try clear H6; try exact H7 ]. cut (argument z' = argument z); intros. 2: apply (argument_affixe_produit_positif_vecteur (k:=k) (A:=A) (B:=B) (A':=A') (B':=B') (z:=z) (z':=z')); auto with geo. apply egalite_forme_polaire. apply points_distincts_non_zeroC with (1 := H5); auto. apply nonzero_produit; auto with geo. apply points_distincts_non_zeroC with (1 := H3); auto with geo. rewrite H2; rewrite Cmult_module; rewrite module_reel; auto. rewrite H6; rewrite Cmult_argument; auto with geo. rewrite argument_reel_pos; auto. rewrite plus_commutative; symmetry in |- *; rewrite plus_angle_zero; auto. apply points_distincts_non_zeroC with (1 := H3); auto with geo. cut (argument z' = plus (argument z) (image_angle pi)); intros. 2: apply (argument_affixe_produit_negatif_vecteur (k:=k) (A:=A) (B:=B) (A':=A') (B':=B') (z:=z) (z':=z')); auto with geo. apply egalite_forme_polaire. apply points_distincts_non_zeroC with (1 := H5); auto. apply nonzero_produit; auto with geo. apply points_distincts_non_zeroC with (1 := H3); auto with geo. rewrite H2; rewrite Cmult_module; rewrite module_reel; auto. rewrite H6; rewrite Cmult_argument; auto with geo. rewrite argument_reel_neg; auto. rewrite plus_commutative; auto. apply points_distincts_non_zeroC with (1 := H3); auto with geo. elim Rtotal_order with (r1 := k) (r2 := 0); [ intros H6; try clear total_order | intros H6; (elim H6; [ intros H7; try clear H6 total_order | intros H7; try clear H6 total_order; try exact H7 ]) ]. right; try assumption. absurd (k = 0); auto. left; try assumption. apply distinct_mult_vecteur with (3 := H1); auto. Qed.