proposition: Lemma reflexion_conserve_alignement: forall (M N A B C A' B' C' :PO) , M<>N-> A' = reflexion M N A -> B' = reflexion M N B -> C' = reflexion M N C -> alignes A B C -> alignes A' B' C'.
proof: Proof. intros M N A B C A' B' C' H0 H1 H2 H3 H. discrimine A B . elim (@reflexion_image_bipoint_coincide M N A B A' B' );auto with geo. discrimine B C . elim (@reflexion_image_bipoint_coincide M N B C B' C' );auto with geo. discrimine C A . elim (@reflexion_image_bipoint_coincide M N C A C' A' );auto with geo. assert (cons_AV (vec A' B') (vec A' C') = opp(cons_AV (vec A B) (vec A C))). apply (@reflexion_anti_deplacement M N A A' B B' C C' );auto. elim(@ alignes_imageZeroPi A B C);intros;auto. rewrite H8 in H7. assert (image_angle (- 0) = opp (image_angle 0)). apply (@mes_opp 0);auto. replace (-0) with (0) in H9. rewrite <-H9 in H7. elim (@angle_nul_positif_colineaire A' B' C'). intros. elim H10;intros. apply colineaire_alignes with x;auto. apply reflexion_image_bipoint_distinct with (M:=M)(N:=N) (A:=A)(B:=B);auto. apply reflexion_image_bipoint_distinct with (M:=M)(N:=N) (A:=A)(B:=C);auto. assumption. field. rewrite H8 in H7. assert (image_angle (pi) = opp(image_angle (pi ))). rewrite <-mes_opp. rewrite <-plus_angle_zero. rewrite <-pi_plus_pi. rewrite <-add_mes_compatible. unfold deuxpi. replace (-pi +(pi +pi)) with (pi). trivial. field. rewrite <-H9 in H7. elim angle_pi_negatif_colineaire with (A:=A')(B:=B')(C:=C'). intros. elim H10;intros. apply colineaire_alignes with x;auto. apply reflexion_image_bipoint_distinct with (M:=M)(N:=N) (A:=A)(B:=B);auto. apply reflexion_image_bipoint_distinct with (M:=M)(N:=N) (A:=A)(B:=C);auto. assumption. Qed.