proposition: Lemma triangle_rotation_trianglesSD: forall (I A B C A' B' C' :PO) ( a : R), triangle A B C -> A' = rotation I a A -> B' = rotation I a B -> C' = rotation I a C -> trianglesSD A B C A' B' C'.
proof: Proof. intros I A B C A' B' C' a H H1 H2. deroule_triangle A B C. unfold trianglesSD. repeat split;[assumption|idtac| apply rotation_conserve_angle with (I:=I)( a:=a);auto with geo| apply rotation_conserve_angle with (I:=I)( a:=a);auto with geo]. intro. elim H0. apply (@rotation_conserve_alignement I A' B' C' A B C (-a) ); [apply rotation_inverse ;auto with geo| apply rotation_inverse;auto with geo| apply rotation_inverse;auto with geo|idtac]. assumption. Qed.