proposition: Lemma reflexion_inverse_angle : forall A B M M' : PO, A <> B -> M <> A -> M <> B -> M' = reflexion A B M -> cons_AV (vec M' A) (vec M' B) = opp (cons_AV (vec M A) (vec M B)).
proof: Proof. intros. elim (classic (alignes A B M)); intros. replace M' with M; auto. cut (double_AV (cons_AV (vec M A) (vec M B)) = image_angle 0); intros. replace (opp (cons_AV (vec M A) (vec M B))) with (plus (image_angle 0) (opp (cons_AV (vec M A) (vec M B)))); auto. rewrite <- H4; unfold double_AV in |- *. mesure M A M B. replace (x + x + - x) with x; auto. ring. mesure M A M B. replace (0 + - x) with (- x); auto. ring. apply angle_alignes; auto with geo. rewrite H2; rewrite <- reflexion_axe; auto. cut (M <> M'); intros. cut (~ alignes A B M'); intros. cut (A <> M'); intros. cut (B <> M'); intros. replace (cons_AV (vec M A) (vec M B)) with (plus (cons_AV (vec M A) (vec M M')) (cons_AV (vec M M') (vec M B))). rewrite opp_plus_plus_opp; auto. rewrite def_opp; auto. lapply (reflexion_isocele (A:=A) (B:=B) (M:=M) (M':=M')); auto; intros. lapply (reflexion_isocele2 (A:=A) (B:=B) (M:=M) (M':=M')); auto; intros. lapply (isocele_angles_base (A:=A) (B:=M) (C:=M')); auto; intros. lapply (isocele_angles_base (A:=B) (B:=M) (C:=M')); auto; intros. rewrite H11; auto. rewrite H10; auto. rewrite def_opp; auto. rewrite Chasles; auto. rewrite Chasles; auto. lapply (non_alignes_distincts2 (A:=A) (B:=B) (C:=M')); auto; intros. lapply (non_alignes_distincts (A:=A) (B:=B) (C:=M')); auto; intros. apply non_axe_image_non_axe with M; auto. apply reflexion_image_distinct with (2 := H2); auto. Qed.