proposition: Theorem rotation_complexe : forall (a : R) (j z z' : C) (J M M' : PO), z = affixe M -> z' = affixe M' -> j = affixe J -> M' = rotation J a M -> Cplus z' (Copp j) = Cmult (cons_pol 1 a) (Cplus z (Copp j)).
proof: Proof. intros a j z z' J M M'; try assumption. discrimine M J. intros. rewrite H1; rewrite H3; rewrite <- rotation_def_centre; rewrite H0; rewrite H2; ring. intros. cut (J <> M); intros. elim rotation_def with (I := J) (A := M) (B := M') (a := a); [ intros | 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)) = module (Cplus z (Copp j))); intros. apply egalite_forme_polaire; auto with geo. rewrite H10; rewrite Cmult_module; rewrite module_un_trivial; ring. rewrite Cmult_argument; auto with geo. rewrite argument_module_un; rewrite H6. 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 H11; repeat rewrite <- mes_opp. rewrite H12; 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 isometrie_distinct with (1 := H4); auto. auto. Qed.