proposition: Lemma cas_a_nonzero_nonone : forall r x : R, r > 0 -> a <> oneC -> a = cons_pol r x -> ex (fun J : PO => forall M : PO, g M = similitude J r x M).
proof: Proof. intros r x H H20 H0; try assumption. elim existence_point_fixe_g; [ intros J H1; try clear existence_point_fixe_g; try exact H1 | auto ]. exists J; intros. elim existence_affixe_point with (M := M); intros z H2; try clear existence_affixe_point; try exact H2. elim existence_affixe_point with (M := g M); intros z'; intros; try exact H2. cut (f (affixe J) = affixe J); intros. apply (complexe_similitude (k:=r) (a:=x) (j:=affixe J) (z:=z) (z':=z') (J:=J) (M:=M) (M':=g M)); auto. rewrite <- H0. apply (equation_solution (z:=z) (z':=z') (j:=affixe J)); auto. rewrite H3; rewrite g_def; rewrite H2; rewrite affixe_transforme; auto. apply point_fixe_gf; auto. Qed.