proposition: Lemma rotation_symetrie : forall A B I : PO, B = rotation I pi A :>PO -> B = symetrie I A :>PO.
proof: Proof. intros. apply milieu_symetrie; auto. discrimine I A. rewrite H; rewrite <- H0; rewrite <- rotation_def_centre; auto with geo. elim rotation_def with (I := I) (A := A) (B := B) (a := pi); [ try clear rotation_def; intros | auto | auto ]. cut (A <> B); intros. apply alignes_mediatrice_milieu; auto. cut (alignes I A B); intros; [ auto with geo | idtac ]. apply alignes_angle; auto with geo. apply image_distinct_centre with (2 := H); auto. unfold double_AV in |- *. rewrite <- H2; rewrite <- pi_plus_pi; auto. rewrite <- add_mes_compatible; auto. red in |- *; intros; apply H0. cut (Rsqr (distance A B) = (2 + 2) * Rsqr (distance I A)); intros. apply distance_nulle; auto. rewrite carre_scalaire_distance. replace (distance I A * distance I A) with (/ (2 + 2) * (distance A B * distance A B)). rewrite <- carre_scalaire_distance. apply Rmult_eq_0_compat. right; try assumption. rewrite H3. replace (vec B B) with (mult_PP 0 (vec B B)); [ idtac | Ringvec ]. Simplscal. replace (distance A B * distance A B) with (Rsqr (distance A B)); auto with real. rewrite H4. cut (2 + 2 <> 0); intros. replace (/ (2 + 2) * ((2 + 2) * Rsqr (distance I A))) with (/ (2 + 2) * (2 + 2) * Rsqr (distance I A)); [ idtac | ring ]. replace (/ (2 + 2) * (2 + 2)) with 1; auto with real. discrR. rewrite (Al_Kashi (A:=I) (B:=A) (C:=B) (a:=pi)); auto. rewrite cos_pi; auto. rewrite <- H1. unfold Rsqr; ring. apply image_distinct_centre with (2 := H); auto. Qed.