proposition: Lemma composee_rotations_meme_centre : forall (I A B C : PO) (a b : R), B = rotation I a A -> C = rotation I b B -> C = rotation I (a + b) A.
proof: Proof. intros. elim (classic (I = A)); intros. rewrite H0. rewrite H. rewrite <- H1. repeat rewrite <- rotation_def_centre; auto. generalize (image_distinct_centre (I:=I) (A:=A) (B:=B) (a:=a)); intros H5. generalize (image_distinct_centre (I:=I) (A:=B) (B:=C) (a:=b)); intros. elim rotation_def with (I := I) (A := A) (B := B) (a := a); [ try clear rotation_def; intros | auto | auto ]. elim rotation_def with (I := I) (A := B) (B := C) (a := b); [ try clear rotation_def; intros | auto | auto ]. apply rotation_def2; auto. rewrite H3; auto. rewrite add_mes_compatible. rewrite H7; rewrite H4; rewrite Chasles; auto. Qed.