proposition: Theorem rotation_conserve_angle : forall (I A B C A' B' C' : PO) (a : R), A <> B :>PO -> A <> C :>PO -> A' = rotation I a A -> B' = rotation I a B -> C' = rotation I a C -> cons_AV (vec A B) (vec A C) = cons_AV (vec A' B') (vec A' C') :>AV.
proof: Proof. intros. generalize (image_bipoint_distinct (I:=I) (A:=A) (B:=C) (A':=A') (B':=C') (a:=a)); intros. generalize (image_bipoint_distinct (I:=I) (A:=A) (B:=B) (A':=A') (B':=B') (a:=a)); intros H11. elim (classic (I = A)); intros. rewrite <- H5 in H1; rewrite <- H5 in H; rewrite <- H5 in H0. rewrite H1; repeat rewrite <- rotation_def_centre; rewrite <- H5; 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 := C) (B := C') (a := a); [ try clear rotation_def; intros | auto | auto ]. generalize (isometrie_distinct (A:=I) (B:=B) (A':=I) (B':=B')); intros H30. generalize (isometrie_distinct (A:=I) (B:=C) (A':=I) (B':=C')); intros H31. apply rotation_IAB with a; auto. elim (classic (I = B)); intros. rewrite <- H6 in H2; rewrite <- H6 in H. rewrite H2; repeat rewrite <- rotation_def_centre; rewrite <- H6; auto. elim rotation_def with (I := I) (A := A) (B := A') (a := a); [ try clear rotation_def; intros | auto | auto ]. elim (classic (I = C)); intros. rewrite <- H9 in H3; rewrite <- H9 in H0. rewrite H3; repeat rewrite <- rotation_def_centre; rewrite <- H9; auto. rewrite <- angle_nul; auto. rewrite <- angle_nul; auto. apply dist_non_nulle; rewrite distance_sym; rewrite <- H7; auto with geo. elim rotation_def with (I := I) (A := C) (B := C') (a := a); [ try clear rotation_def; intros | auto | auto ]. generalize (isometrie_distinct (A:=I) (B:=C) (A':=I) (B':=C')); intros H31. elim cas_egalite_triangle with (A := I) (B := A) (C := C) (A' := I) (B' := A') (C' := C'); (auto with geo; intros). elim H14; intros H15 H16; try clear H14; try exact H16. mesure A C A I. rewrite <- (mes_oppx (A:=A) (B:=C) (C:=A) (D:=I) (x:=x)); auto. rewrite <- (mes_oppx (A:=A') (B:=C') (C:=A') (D:=I) (x:=x)); auto. apply dist_non_nulle; rewrite distance_sym; rewrite <- H7; auto with geo. rewrite H14; rewrite H15; auto. generalize (isometrie_distinct (A:=I) (B:=A) (A':=I) (B':=A')); intros H30. apply rotation_IAB with a; 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 H31. elim (classic (I = C)); intros. rewrite <- H7 in H3. rewrite H3; repeat rewrite <- rotation_def_centre; rewrite <- H7; auto. elim rotation_def with (I := I) (A := A) (B := A') (a := a); [ try clear rotation_def; intros | auto | auto ]. elim rotation_def with (I := I) (A := B) (B := B') (a := a); [ try clear rotation_def; intros | auto | auto ]. elim cas_egalite_triangle with (A := I) (B := A) (C := B) (A' := I) (B' := A') (C' := B'); (auto; intros). elim H14; intros H15 H16; try clear H14; try exact H15. apply rotation_IAB with a; auto. generalize (isometrie_distinct (A:=I) (B:=C) (A':=I) (B':=C')); intros H32. elim rotation_def with (I := I) (A := A) (B := A') (a := a); [ try clear rotation_def; intros | auto | 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 := C) (B := C') (a := a); [ try clear rotation_def; intros | auto | auto ]. elim cas_egalite_triangle with (A := I) (B := A) (C := B) (A' := I) (B' := A') (C' := B'); (auto; intros). elim cas_egalite_triangle with (A := I) (B := A) (C := C) (A' := I) (B' := A') (C' := C'); (auto; intros). elim H18; intros H19 H20; try clear H18; try exact H20. elim H16; intros H18 H21; try clear H16; try exact H21. replace (cons_AV (vec A B) (vec A C)) with (plus (cons_AV (vec A B) (vec A I)) (cons_AV (vec A I) (vec A C))). mesure A C A I. rewrite <- (mes_oppx (A:=A) (B:=C) (C:=A) (D:=I) (x:=x)); auto with geo. rewrite (mes_oppx (A:=A') (B:=C') (C:=A') (D:=I) (x:=x)); auto with geo. rewrite H18; rewrite Chasles; auto with geo. apply dist_non_nulle; rewrite distance_sym; rewrite <- H8; auto with geo. apply dist_non_nulle; rewrite distance_sym; rewrite <- H8; auto with geo. rewrite H16; rewrite H19; auto. rewrite Chasles; auto. apply rotation_IAB with a; auto. apply rotation_IAB with a; auto. Qed.