proposition: Theorem rotation_isometrie : forall (I A B A' B' : PO) (a : R), A' = rotation I a A -> B' = rotation I a B -> distance A' B' = distance A B.
proof: Proof. intros I A B A' B' a H H0; try assumption. apply distance_carre; auto. elim (classic (I = A)); intros. rewrite <- H1 in H. rewrite <- H1; rewrite H; repeat rewrite <- rotation_def_centre; auto. elim (classic (I = B)); intros. rewrite <- H2 in H0. rewrite H0; rewrite <- H2; repeat rewrite <- rotation_def_centre; auto. elim rotation_def with (I := I) (A := B) (B := B') (a := a); [ try clear rotation_def; intros | auto | auto ]. rewrite H3; auto. elim (classic (I = B)); intros. rewrite <- H2 in H0. rewrite H0; rewrite <- H2; repeat rewrite <- rotation_def_centre; auto. elim rotation_def with (I := I) (A := A) (B := A') (a := a); [ try clear rotation_def; intros | auto | auto ]. rewrite (distance_sym A I); auto. rewrite H3; rewrite distance_sym; auto. generalize (image_distinct_centre (I:=I) (A:=A) (B:=A') (a:=a)); intros H11. generalize (image_distinct_centre (I:=I) (A:=B) (B:=B') (a:=a)); intros H12. elim rotation_def with (I := I) (A := B) (B := B') (a := a); [ try clear rotation_def; intros | auto | auto ]. elim rotation_def with (I := I) (A := A) (B := A') (a := a); [ try clear rotation_def; intros | auto | auto ]. mesure I A I B. rewrite (Al_Kashi (A:=I) (B:=A) (C:=B) (a:=x)); auto. rewrite (Al_Kashi (A:=I) (B:=A') (C:=B') (a:=x)); auto. rewrite H5; rewrite H3; auto. rewrite H7. replace (cons_AV (vec I A') (vec I B')) with (plus (cons_AV (vec I A') (vec I A)) (plus (cons_AV (vec I A) (vec I B)) (cons_AV (vec I B) (vec I B')))). rewrite <- (mes_oppx (A:=I) (B:=A) (C:=I) (D:=A') (x:=a)); auto. rewrite <- H7; rewrite <- H4. rewrite <- add_mes_compatible; rewrite <- add_mes_compatible. replace (- a + (x + a)) with x; try ring; auto. rewrite Chasles; auto. rewrite Chasles; auto. Qed.