proposition: Lemma composee_rotation_homothetie_pos : forall (I M M' M1 : PO) (k a : R), k > 0 -> M1 = rotation I a M -> M' = homothetie k I 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 <- rotation_def_centre; intros. rewrite H2; rewrite H1; rewrite <- homothetie_centre; auto. intros. elim rotation_def with (I := I) (A := M) (B := M1) (a := a); [ intros | auto | auto ]. cut (distance I M' = Rabs k * distance I M1); intros. 2: apply distance_homothetie with I; auto with geo. apply similitude_def2; auto. rewrite H5; rewrite H3; rewrite Rabs_right; auto. lra. rewrite H4; auto. cut (vec I M' = mult_PP k (vec I M1)); intros. symmetry in |- *; rewrite (angle_produit_positif_r (k:=k) (A:=I) (B:=M1) (C:=M') (D:=I) (E:=M)) ; auto. apply image_distinct_centre with (2 := H1); auto. apply homothetie_vecteur; auto. Qed.