proposition: Lemma rotation_conserve_alignement: forall (I A B C A' B' C' :PO) ( a : R), A' = rotation I a A -> B' = rotation I a B -> C' = rotation I a C -> alignes A B C -> alignes A' B' C'.
proof: Proof. intros I A B C A' B' C' a H H0 H1 H2 . discrimine A B . elim (@rotation_image_bipoint_coincide I A B A' B' a);auto with geo. discrimine B C . elim (@rotation_image_bipoint_coincide I B C B' C' a);auto with geo. discrimine C A . elim (@rotation_image_bipoint_coincide I C A C' A' a);auto with geo. assert (cons_AV (vec A B) (vec A C) = cons_AV (vec A' B') (vec A' C')). apply (@rotation_conserve_angle I A B C A' B' C' a);auto. elim(@ alignes_imageZeroPi A B C);intros;auto. rewrite H7 in H6. elim (@angle_nul_positif_colineaire A' B' C'). intros. elim H8;intros. apply colineaire_alignes with x;auto. apply image_bipoint_distinct with (I:=I)(a:=a) (A:=A)(B:=B);auto. apply image_bipoint_distinct with (I:=I)(a:=a) (A:=A)(B:=C);auto. auto. elim angle_pi_negatif_colineaire with (A:=A')(B:=B')(C:=C'). intros. elim H8;intros. apply colineaire_alignes with x;auto. apply image_bipoint_distinct with (I:=I)(a:=a) (A:=A)(B:=B);auto. apply image_bipoint_distinct with (I:=I)(a:=a) (A:=A)(B:=C);auto. rewrite <-H6;assumption. Qed.