proposition: Theorem reflexion_anti_deplacement : forall A B M M' N N' P P' : PO, A <> B -> M <> N -> M <> P -> N <> P -> M' = reflexion A B M -> N' = reflexion A B N -> P' = reflexion A B P -> cons_AV (vec M' N') (vec M' P') = opp (cons_AV (vec M N) (vec M P)).
proof: Proof. intros. cut (M' <> N'); intros. cut (M' <> P'); intros. discrimine M A. cut (M' = A); intros. rewrite H9. cut (A <> N); intros. cut (A <> P); intros. apply reflexion_inverse_AMN with B; auto. red in |- *; intros; apply H1. rewrite H8; auto. red in |- *; intros; apply H0. rewrite H8; auto. rewrite H3; rewrite H8; rewrite <- reflexion_axe; auto with geo. discrimine N A. cut (N' = A); intros. rewrite H10. cut (A <> P); intros. elim cas_egalite_triangle_indirect with (A := A) (B := M) (C := P) (A' := A) (B' := M') (C' := P'); (auto; intros). elim H13; intros. rewrite <- H14; rewrite def_opp; auto. rewrite (reflexion_isometrie (A:=A) (B:=B) (M:=A) (M':=A) (N:=M) (N':=M')); auto with geo. rewrite (reflexion_isometrie (A:=A) (B:=B) (M:=A) (M':=A) (N:=P) (N':=P')); auto with geo. rewrite (reflexion_inverse_AMN (A:=A) (B:=B) (M:=P) (M':=P') (N:=M) (N':=M')); auto. rewrite def_opp; auto. red in |- *; intros; apply H2. rewrite H9; auto. rewrite H4; rewrite H9; rewrite <- reflexion_axe; auto with geo. discrimine P A. cut (P' = A); intros. rewrite H11. elim cas_egalite_triangle_indirect with (A := A) (B := M) (C := N) (A' := A) (B' := M') (C' := N'); (auto; intros). elim H13; intros. rewrite H14; rewrite def_opp; auto. red in |- *; intros; apply H7. rewrite H16; auto. rewrite (reflexion_isometrie (A:=A) (B:=B) (M:=A) (M':=A) (N:=M) (N':=M')); auto with geo. rewrite (reflexion_isometrie (A:=A) (B:=B) (M:=A) (M':=A) (N:=N) (N':=N')); auto with geo. rewrite (reflexion_inverse_AMN (A:=A) (B:=B) (M:=N) (M':=N') (N:=M) (N':=M')); auto. rewrite def_opp; auto. rewrite H5; rewrite H10; rewrite <- reflexion_axe; auto with geo. cut (A <> M'); intros. elim cas_egalite_triangle_indirect with (A := A) (B := M) (C := N) (A' := A) (B' := M') (C' := N'); (auto; intros). elim H13; intros. elim cas_egalite_triangle_indirect with (A := A) (B := M) (C := P) (A' := A) (B' := M') (C' := P'); (auto; intros). elim H17; intros. replace (cons_AV (vec M N) (vec M P)) with (plus (cons_AV (vec M N) (vec M A)) (cons_AV (vec M A) (vec M P))). replace (cons_AV (vec M A) (vec M P)) with (cons_AV (vec M' P') (vec M' A)). rewrite H14. replace (plus (cons_AV (vec M' A) (vec M' N')) (cons_AV (vec M' P') (vec M' A))) with (plus (cons_AV (vec M' P') (vec M' A)) (cons_AV (vec M' A) (vec M' N'))). rewrite Chasles; auto. rewrite def_opp; auto. mesure M' P' M' A. mesure M' A M' N'. replace (x + x0) with (x0 + x); auto. ring. apply permute_angles; auto. rewrite Chasles; auto. rewrite (reflexion_isometrie (A:=A) (B:=B) (M:=A) (M':=A) (N:=M) (N':=M')); auto with geo. rewrite (reflexion_isometrie (A:=A) (B:=B) (M:=A) (M':=A) (N:=P) (N':=P')); auto with geo. rewrite (reflexion_inverse_AMN (A:=A) (B:=B) (M:=P) (M':=P') (N:=M) (N':=M')); auto. rewrite def_opp; auto. rewrite (reflexion_isometrie (A:=A) (B:=B) (M:=A) (M':=A) (N:=M) (N':=M')); auto with geo. rewrite (reflexion_isometrie (A:=A) (B:=B) (M:=A) (M':=A) (N:=N) (N':=N')); auto with geo. rewrite (reflexion_inverse_AMN (A:=A) (B:=B) (M:=N) (M':=N') (N:=M) (N':=M')); auto. rewrite def_opp; auto. apply (isometrie_distinct (A:=A) (B:=M) (A':=A) (B':=M')); auto with geo. rewrite (reflexion_isometrie (A:=A) (B:=B) (M:=A) (M':=A) (N:=M) (N':=M')); auto with geo. apply (isometrie_distinct (A:=M) (B:=P) (A':=M') (B':=P')); auto. rewrite (reflexion_isometrie (A:=A) (B:=B) (M:=M) (M':=M') (N:=P) (N':=P')); auto. apply (isometrie_distinct (A:=M) (B:=N) (A':=M') (B':=N')); auto. rewrite (reflexion_isometrie (A:=A) (B:=B) (M:=M) (M':=M') (N:=N) (N':=N')); auto. Qed.