proposition: Lemma similitude_decomposition : forall (I M M' : PO) (k a : R), k > 0 -> M' = similitude I k a M -> exists M1 : PO, M1 = rotation I a M /\ M' = homothetie k I M1.
proof: Proof. intros. elim existence_rotation_Ia with (I := I) (M := M) (a := a); intros M1; intros. exists M1. split; [ try assumption | idtac ]. discrimine I M. rewrite <- H2 in H1; rewrite <- H2 in H0. rewrite <- similitude_def_centre in H0; auto; rewrite <- rotation_def_centre in H1. rewrite <- H2; rewrite H0; rewrite H1; auto with geo. cut (I <> M1); intros. cut (I <> M'); intros. apply vecteur_homothetie. elim similitude_def with (I := I) (A := M) (B := M') (k := k) (a := a); [ intros | auto | auto | auto ]. elim rotation_def with (I := I) (A := M) (B := M1) (a := a); [ intros | auto | auto ]. apply alignes_distance_positif_colineaire; auto. replace (cons_AV (vec I M1) (vec I M')) with (plus (cons_AV (vec I M) (vec I M')) (opp (cons_AV (vec I M) (vec I M1)))). rewrite def_opp; auto. rewrite <- (mes_oppx (A:=I) (B:=M) (C:=I) (D:=M1) (x:=a)); auto. rewrite <- H6. repeat rewrite <- add_mes_compatible. replace (a + - a) with 0; auto. ring. apply Chasles_diff; auto. rewrite <- H7; auto. apply image_sim_distinct_centre with (3 := H0); auto. apply image_distinct_centre with (2 := H1); auto. Qed.