proposition: Lemma un_module_a_deplacement : module a = 1 -> (exists A : PO, (forall M : PO, g M = translation O A M)) \/ (exists J : PO, (exists x : R, (forall M : PO, g M = rotation J x M))).
proof: Proof. intros. elim (classic (a = oneC)); intros. left; try assumption. apply a_oneC_translation; auto. right; try assumption. cut (a <> zeroC). intros H20. elim existence_forme_polaire with (z := a); [ intros r H1; elim H1; intros x H2; elim H2; intros H3 H4; try clear H2 H1; try exact H4 | auto with geo ]. elim un_module_a_rotation with (x := x); [ intros J H1; try clear un_module_a_rotation; try exact H1 | auto with geo | auto with geo ]. exists J; exists x; auto with geo. apply nonzero_module. rewrite H; discrR. Qed.