proposition: Lemma similitude_angle_nul : forall (I A : PO) (k : R), k > 0 -> homothetie k I A = similitude I k 0 A.
proof: Proof. intros. discrimine I A. rewrite <- homothetie_centre; rewrite <- similitude_def_centre; auto. cut (A = rotation I 0 A); intros. 2: apply rotation_angle_nul. elim existence_homothetique with (k := k) (I := I) (A := A); intros M'; intros. rewrite <- H2. apply composee_rotation_homothetie_pos with A; auto. Qed.