proposition: Lemma rotation_homothetie_pos_I_commutent : forall (I M M1 M2 : PO) (k a : R), k > 0 -> M1 = homothetie k I M -> M2 = rotation I a M -> homothetie k I M2 = rotation I a M1.
proof: Proof. intros. elim existence_rotation_Ia with (I := I) (M := M1) (a := a); intros N; intros. elim existence_homothetique with (k := k) (I := I) (A := M2); intros N'; intros. rewrite <- H3; rewrite <- H2. rewrite (composee_rotation_homothetie_pos (I:=I) (M:=M) (M':=N') (M1:=M2) (k:=k) (a:=a)); auto. rewrite (composee_homothetie_pos_rotation (I:=I) (M:=M) (M':=N) (M1:=M1) (k:=k) (a:=a)); auto. Qed.