proposition: Theorem similitude_complexe : forall (k a : R) (j z z' : C) (J M M' : PO), k > 0 -> z = affixe M -> z' = affixe M' -> j = affixe J -> M' = similitude J k a M -> Cplus z' (Copp j) = Cmult (cons_pol k a) (Cplus z (Copp j)).
proof: Proof. intros k a j z z' J M M' H; try assumption. discrimine M J. intros. rewrite H2; rewrite H4; rewrite <- similitude_def_centre; auto; rewrite H1; rewrite H3; ring. intros. cut (J <> M); intros. elim similitude_def with (I := J) (A := M) (B := M') (k := k) (a := a); [ intros | auto | auto | auto ]. cut (J <> M'); intros. cut (Cplus z (Copp j) <> zeroC); intros. cut (Cplus z' (Copp j) <> zeroC); intros. cut (module (Cplus z' (Copp j)) = k * module (Cplus z (Copp j))); intros. cut (cons_pol k a <> zeroC); intros; auto with real geo. apply egalite_forme_polaire; auto with geo. rewrite H11; rewrite Cmult_module; rewrite complexe_polaire_module; ring. rewrite Cmult_argument; auto with geo. rewrite complexe_polaire_argument; auto with real geo. rewrite H7. rewrite (angle_vecteurs_arguments (A:=J) (B:=M) (A':=J) (B':=M') (z:=Cplus z (Copp j)) (z':=Cplus z' (Copp j))); auto with geo. elim existence_argument with (z := Cplus z (Copp j)); [ intros; try clear existence_argument | auto ]. elim existence_argument with (z := Cplus z' (Copp j)); [ intros; try clear existence_argument | auto ]. rewrite H13; rewrite H14; repeat rewrite <- mes_opp; repeat rewrite <- add_mes_compatible. replace (x0 + - x + x) with x0; [ auto | ring ]. rewrite (module_difference (a:=j) (b:=z) (A:=J) (B:=M)); auto. rewrite (module_difference (a:=j) (b:=z') (A:=J) (B:=M')); auto. eauto with geo. eauto with geo. apply image_sim_distinct_centre with (3 := H4); auto. auto. Qed.