proposition: Lemma composee_homothetie_pos_rotation : forall (I M M' M1 : PO) (k a : R), k > 0 -> M1 = homothetie k I M -> M' = rotation I a M1 -> M' = similitude I k a M.
proof: Proof. intros I M M' M1 k a H; try assumption. discrimine I M. rewrite <- similitude_def_centre; auto; rewrite <- homothetie_centre; intros. rewrite H2; rewrite H1; rewrite <- rotation_def_centre; auto. intros. cut (vec I M1 = mult_PP k (vec I M)); intros. cut (distance I M1 = Rabs k * distance I M); intros. 2: apply distance_homothetie with I; auto with geo. cut (I <> M1); intros. cut (I <> M'); intros. elim rotation_def with (I := I) (A := M1) (B := M') (a := a); [ intros | auto | auto ]. apply similitude_def2; auto. rewrite <- H7; rewrite H4; rewrite Rabs_right; auto. lra. rewrite H8. apply permute_angles; auto. rewrite (angle_produit_positif_r (k:=k) (A:=I) (B:=M) (C:=M1) (D:=I) (E:=M')); auto. apply image_distinct_centre with (2 := H2); auto with geo. apply distinct_produit_vecteur with (3 := H3); auto. auto with real. apply homothetie_vecteur; auto. Qed.