proposition: Lemma reflexion_isometrie : forall A B M M' N N' : PO, A <> B -> M' = reflexion A B M -> N' = reflexion A B N -> distance M N = distance M' N'.
proof: Proof. intros. discrimine M N. rewrite H2 in H0. rewrite H0; rewrite <- H1. rewrite distance_refl2; auto. rewrite distance_refl2; auto. elim (classic (alignes A B M)); intros. replace M' with M; auto. elim (classic (alignes A B N)); intros. replace N' with N; auto. rewrite H1; rewrite <- reflexion_axe; auto. cut (A <> N); intros. cut (A <> N'); intros. discrimine M A. elim (reflexion_mediatrice (A:=A) (B:=B) (M:=N) (M':=N')); auto; unfold mediatrice in |- *; intros. lapply (axe_reflexion_droite (A:=A) (B:=B) (C:=M) (M:=N) (M':=N')); auto; intros. elim (reflexion_mediatrice (A:=M) (B:=A) (M:=N) (M':=N')); auto with geo; unfold mediatrice in |- *; intros. lapply (alignes_non_alignes_trans (A:=A) (B:=B) (C:=N) (D:=M)); auto with geo; intros. lapply (non_alignes_distincts (A:=A) (B:=B) (C:=N')); auto with geo; intros. apply non_axe_image_non_axe with N; auto with geo. apply non_alignes_distincts with B; auto with geo. rewrite H0; rewrite <- reflexion_axe; auto. cut (A <> M); intros. cut (A <> M'); intros. elim (classic (alignes A B N)); intros. replace N' with N; auto. discrimine N A. rewrite distance_sym; rewrite (distance_sym M' A). elim (reflexion_mediatrice (A:=A) (B:=B) (M:=M) (M':=M')); auto with geo; unfold mediatrice in |- *; intros. lapply (axe_reflexion_droite (A:=A) (B:=B) (C:=N) (M:=M) (M':=M')); auto with geo; intros. rewrite distance_sym; rewrite (distance_sym M' N). elim (reflexion_mediatrice (A:=N) (B:=A) (M:=M) (M':=M')); auto with geo; unfold mediatrice in |- *; intros. lapply (alignes_non_alignes_trans (A:=A) (B:=B) (C:=M) (D:=N)); auto with geo; intros. rewrite H1; rewrite <- reflexion_axe; auto. cut (A <> N); intros. cut (A <> N'); intros. elim cas_egalite_triangle_indirect with (A := A) (B := M) (C := N) (A' := A) (B' := M') (C' := N'); (auto; intros). elim (reflexion_mediatrice (A:=A) (B:=B) (M:=M) (M':=M')); auto with geo; unfold mediatrice in |- *; intros. elim (reflexion_mediatrice (A:=A) (B:=B) (M:=N) (M':=N')); auto with geo; unfold mediatrice in |- *; intros. replace (cons_AV (vec A M) (vec A N)) with (plus (cons_AV (vec A M) (vec A B)) (cons_AV (vec A B) (vec A N))). rewrite (axe_reflexion_bissectrice (A:=A) (B:=B) (M:=M) (M':=M')); auto. replace (cons_AV (vec A B) (vec A N)) with (cons_AV (vec A N') (vec A B)). replace (plus (cons_AV (vec A B) (vec A M')) (cons_AV (vec A N') (vec A B))) with (plus (cons_AV (vec A N') (vec A B)) (cons_AV (vec A B) (vec A M'))). rewrite Chasles; auto. mesure A B A M'. mesure A N' A B. replace (x0 + x) with (x + x0); auto. ring. apply permute_angles; auto. rewrite (axe_reflexion_bissectrice (A:=A) (B:=B) (M:=N) (M':=N')); auto. rewrite Chasles; auto. lapply (non_alignes_distincts (A:=A) (B:=B) (C:=N')); auto; intros. apply non_axe_image_non_axe with N; auto. apply non_alignes_distincts with B; auto. lapply (non_alignes_distincts (A:=A) (B:=B) (C:=M')); auto; intros. apply non_axe_image_non_axe with M; auto. apply non_alignes_distincts with B; auto. Qed.