proposition: Theorem produit_reel_affixe_vecteur_OM : forall (k : R) (z z' : C) (M M' : PO), z = affixe_vec (vec O M) :>C -> z' = affixe_vec (vec O M') :>C -> z' = Cmult (Rinj k) z :>C -> vec O M' = mult_PP k (vec O M) :>PP.
proof: Proof. intros. cut (module z' = module (Rinj k) * module z); intros. discrimine O M. cut (z = zeroC); intros. replace M with M'. Ringvec. apply (egalite_affixe_point (z:=z') (z':=z) (M:=M') (M':=M)); auto with geo. rewrite H1; rewrite H4; ring. apply (egalite_point_image (z:=z) (z':=zeroC) (M:=M) (M':=O)); auto with geo. cut (z <> zeroC); [ idtac | eauto with geo ]. intros H20. elim Rtotal_order with (r1 := k) (r2 := 0); [ intros H6; try clear total_order | intros H6; (elim H6; [ intros H7; try clear H6 | intros H7; try clear H6; try exact H7 ]) ]. rewrite module_reel_neg in H2; auto with real. cut (k <> 0); intros; [ idtac | auto with real ]. cut (z' <> zeroC); intros. cut (O <> M'); intros. cut (cons_AV (vec O M) (vec O M') = image_angle pi); intros. rewrite (alignes_distance_negatif_colineaire (k:=- k) (A:=O) (B:=M) (C:=M')); auto with geo. replace (- - k) with k; try ring; auto. rewrite <- (module_def2 (z:=z) (M:=M)); auto with geo. rewrite <- (module_def2 (z:=z') (M:=M')); auto with geo. rewrite (angle_argument (z:=z) (z':=z') (M:=M) (M':=M')); auto with geo. rewrite H1; rewrite Cmult_argument; auto with geo. rewrite argument_reel_neg; auto with geo. elim existence_argument with (z := z); [ intros; try clear existence_argument | auto with geo ]. rewrite H8; rewrite <- mes_opp; repeat rewrite <- add_mes_compatible. replace (pi + x + - x) with pi; [ auto | ring ]. apply image_nonzero_nonorigine with z'; auto with geo. apply nonzero_module. rewrite H2. apply Rmult_integral_contrapositive. split; auto with real geo. cut (z' = zeroC); intros. replace M' with O. rewrite H7; Ringvec. apply (egalite_affixe_point (z:=zeroC) (z':=z') (M:=O) (M':=M')); auto with geo. apply module_nul_zeroC. rewrite H2; rewrite H7. replace (Rinj 0) with zeroC; auto with geo. rewrite module_zeroC; ring. rewrite module_reel_pos in H2; auto with real. cut (k <> 0); intros; [ idtac | auto with real ]. cut (z' <> zeroC); intros. cut (O <> M'); intros. cut (cons_AV (vec O M) (vec O M') = image_angle 0); intros. rewrite (alignes_distance_positif_colineaire (k:=k) (A:=O) (B:=M) (C:=M')); auto with geo. rewrite <- (module_def2 (z:=z) (M:=M)); auto with geo. rewrite <- (module_def2 (z:=z') (M:=M')); auto with geo. rewrite (angle_argument (z:=z) (z':=z') (M:=M) (M':=M')); auto with geo. rewrite H1; rewrite Cmult_argument; auto with geo. rewrite argument_reel_pos; auto with geo. elim existence_argument with (z := z); [ intros; try clear existence_argument | auto with geo ]. rewrite H8; rewrite <- mes_opp; repeat rewrite <- add_mes_compatible. replace (0 + x + - x) with 0; [ auto | ring ]. apply image_nonzero_nonorigine with z'; auto with geo. apply nonzero_module. rewrite H2. apply Rmult_integral_contrapositive. split; auto with real geo. rewrite H1; rewrite Cmult_module; auto. Qed.