proposition: Lemma rotation_inverse : forall (I A B : PO) (a : R), B = rotation I a A :>PO -> A = rotation I (- a) B :>PO.
proof: Proof. intros. elim (classic (I = A)); intros. rewrite <- H0. rewrite <- H0 in H. rewrite H; rewrite <- rotation_def_centre; auto. apply rotation_def_centre. elim rotation_def with (I := I) (A := A) (B := B) (a := a); [ try clear rotation_def; intros | auto | auto ]. apply rotation_def2; auto. apply image_distinct_centre with (2 := H); auto. rewrite <- (mes_oppx (A:=I) (B:=A) (C:=I) (D:=B) (x:=a)); auto. apply image_distinct_centre with (2 := H); auto. Qed.