proposition: Theorem rotation_image_bipoint : forall (I A B C A' B' C' : PO) (a : R), A <> B :>PO -> A' = rotation I a A -> B' = rotation I a B -> distance A' B' = distance A B /\ image_angle a = cons_AV (vec A B) (vec A' B') :>AV.
proof: Proof. intros. generalize (image_bipoint_distinct (I:=I) (A:=A) (B:=B) (A':=A') (B':=B') (a:=a)); intros H11. split; [ try assumption | idtac ]. apply rotation_isometrie with (1 := H0); auto. elim (classic (I = A)); intros. rewrite <- H2; rewrite <- H2 in H0; rewrite <- H2 in H. elim rotation_def with (I := I) (A := B) (B := B') (a := a); [ try clear rotation_def; intros | auto | auto ]. rewrite H0; repeat rewrite <- rotation_def_centre; auto. elim (classic (I = B)); intros. rewrite <- H3; rewrite <- H3 in H1; rewrite <- H3 in H. generalize (isometrie_distinct (A:=I) (B:=A) (A':=I) (B':=A')); intros H30. elim rotation_def with (I := I) (A := A) (B := A') (a := a); [ try clear rotation_def; intros | auto | auto ]. rewrite H1; repeat rewrite <- rotation_def_centre; auto. rewrite angle_oppu_oppv; auto. 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 ]. generalize (isometrie_distinct (A:=I) (B:=A) (A':=I) (B':=A')); intros H30. generalize (isometrie_distinct (A:=I) (B:=B) (A':=I) (B':=B')); intros. elim cas_egalite_triangle with (A := I) (B := A) (C := B) (A' := I) (B' := A') (C' := B'); (auto; intros). elim H10; intros H12 H13; try clear H10; try exact H13. replace (cons_AV (vec A B) (vec A' B')) with (plus (cons_AV (vec A B) (vec A I)) (plus (cons_AV (vec A I) (vec A' I)) (cons_AV (vec A' I) (vec A' B')))). mesure A B A I. rewrite <- (mes_oppx (A:=A') (B:=B') (C:=A') (D:=I) (x:=x)). rewrite angle_oppu_oppv; auto. rewrite <- H7. rewrite <- add_mes_compatible; rewrite <- add_mes_compatible. replace (x + (a + - x)) with a; try ring; auto. apply H11; auto. apply dist_non_nulle; rewrite distance_sym; rewrite <- H6; auto with geo. rewrite H10; rewrite H12; auto. rewrite Chasles; auto. rewrite Chasles; auto. apply dist_non_nulle; rewrite distance_sym; rewrite <- H6; auto with geo. apply rotation_IAB with a; auto. Qed.