proposition: Lemma symetrie_rotation : forall A B I : PO, B = symetrie I A :>PO -> B = rotation I pi A :>PO.
proof: Proof. intros. generalize symetrie_milieu; intros. discrimine I A. rewrite <- rotation_def_centre. rewrite H; rewrite H1. symmetry in |- *. apply milieu_symetrie; auto with geo. apply rotation_def2; auto with geo. rewrite <- (milieu_vecteur (A:=A) (B:=B) (M:=I)). apply angle_plat; auto. apply H0; auto. Qed.