proposition: Lemma reflexion_inverse_AMN : forall A B M M' N N' : PO, A <> B -> A <> M -> A <> N -> M' = reflexion A B M -> N' = reflexion A B N -> cons_AV (vec A M') (vec A N') = opp (cons_AV (vec A M) (vec A N)).
proof: Proof. intros. elim (classic (alignes A B M)); intros. replace M' with M; auto. elim (classic (alignes A B N)); intros. replace N' with N; auto. lapply (alignes_trans (A:=A) (B:=B) (C:=M) (D:=N)); auto; intros. cut (double_AV (cons_AV (vec A M) (vec A N)) = image_angle 0); intros. replace (opp (cons_AV (vec A M) (vec A N))) with (plus (image_angle 0) (opp (cons_AV (vec A M) (vec A N)))); auto. rewrite <- H7; unfold double_AV in |- *. mesure A M A N. replace (x + x + - x) with x; auto. ring. rewrite plus_commutative; auto with geo. apply angle_alignes; auto. rewrite H3; rewrite <- reflexion_axe; auto. cut (A <> N'); intros. lapply (axe_reflexion_droite (A:=A) (B:=B) (C:=M) (M:=N) (M':=N')); auto; intros. rewrite <- (axe_reflexion_bissectrice (A:=A) (B:=M) (M:=N) (M':=N')); auto. rewrite def_opp; auto. lapply (alignes_non_alignes_trans (A:=A) (B:=B) (C:=N) (D:=M)); auto; intros. lapply (axe_reflexion_droite (A:=M) (B:=A) (C:=A) (M:=N) (M':=N')); auto with geo; intros. lapply (non_alignes_distincts (A:=A) (B:=B) (C:=N')); auto; intros. apply non_axe_image_non_axe with N; auto. rewrite H2; rewrite <- reflexion_axe; auto. cut (A <> M'); intros. elim (classic (alignes A B N)); intros. replace N' with N; auto. lapply (axe_reflexion_droite (A:=A) (B:=B) (C:=N) (M:=M) (M':=M')); auto; intros. rewrite (axe_reflexion_bissectrice (A:=A) (B:=N) (M:=M) (M':=M')); auto. rewrite def_opp; auto. lapply (alignes_non_alignes_trans (A:=A) (B:=B) (C:=M) (D:=N)); auto; intros. lapply (axe_reflexion_droite (A:=N) (B:=A) (C:=A) (M:=M) (M':=M')); auto with geo; intros. rewrite H3; rewrite <- reflexion_axe; auto. cut (A <> N'); 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. rewrite def_opp; 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. apply non_axe_image_non_axe with M; auto. Qed.