proposition: Lemma triangle_reflexion_trianglesSI: forall (M N A B C A' B' C' :PO) , M<>N-> triangle A B C -> A' = reflexion M N A -> B' = reflexion M N B -> C' = reflexion M N C -> trianglesSI A B C A' B' C'.
proof: Proof. intros M N A B C A' B' C' H H0 H1 H2 H3. deroule_triangle A B C. unfold trianglesSI. repeat split;[assumption|idtac| rewrite-> (@reflexion_anti_deplacement M N B B' A A' C C');auto with geo;rewrite->def_opp ; auto| rewrite-> (@reflexion_anti_deplacement M N C C' B B' A A' );auto with geo;rewrite->def_opp ; auto]. intro. elim H4. apply (@reflexion_conserve_alignement M N A' B' C' A B C ); [assumption|apply reflexion_symetrie ;auto with geo| apply reflexion_symetrie;auto with geo| apply reflexion_symetrie;auto with geo|idtac]. assumption. Qed.