proposition: Theorem cas_general_deplacement_similitude : a <> zeroC -> (ex (fun A : PO => forall M : PO, g M = translation O A M) \/ ex (fun J : PO => ex (fun x : R => forall M : PO, g M = rotation J x M))) \/ (exists r : R, (exists x : R, (exists J : PO, (forall M : PO, g M = similitude J r x M)))).
proof: Proof. intros. elim existence_forme_polaire with (z := a); [ intros r H0; elim H0; intros x H1; elim H1; intros H2 H3; try clear H1 H0; try exact H3 | auto with geo ]. cut (a = cons_pol r x); intros; auto with geo. elim (classic (module a = 1)); intros. left; try assumption. apply un_module_a_deplacement; auto with geo. right; try assumption. exists r; exists x. apply cas_a_nonzero_nonone; auto. rewrite <- H2; auto with geo. red in |- *; intros; apply H1. rewrite H4; auto with geo. Qed.