proposition: Lemma rotation_homothetie_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 I M M1 M2 k a H; try assumption. repeat rewrite similitude_rapport_un. elim Rtotal_order with (r1 := k) (r2 := 0); [ intros H4; try clear total_order | intros H4; (elim H4; [ intros H5; try clear H4 total_order | intros H5; try clear H4 total_order; try exact H5 ]) ]. repeat (rewrite homothetie_neg2; auto). intros. apply similitudes_meme_centre_commutent with (3 := H0) (4 := H1); auto. auto with real. lra. absurd (k = 0); auto with real. repeat (rewrite similitude_angle_nul; auto). intros. apply similitudes_meme_centre_commutent with (3 := H0) (4 := H1); auto. lra. Qed.