proposition: Lemma inversion_oppose_puissance : forall (I A B C : PO) (k : R), k <> 0 -> I <> A -> B = inversion I k A -> C = symetrie I A -> B = inversion I (- k) C.
proof: Proof. intros. generalize H2; unfold symetrie in |- *; intros. assert (I <> C). assert (I = homothetie (-1) I I); auto with geo. apply (image_homothetie_distincts (k:=-1) (I:=I) (A:=I) (A':=I) (B:=A) (B':=C)); auto with real. generalize (inversion_homothetie (I:=I) (A:=A) (B:=B) (k:=k)); intros. apply homothetie_inversion; auto with real. generalize (homothetie_vecteur (k:=/ Rsqr (distance I A) * k) (I:=I) (A:=A) (A':=B)); intros. apply vecteur_homothetie. rewrite (homothetie_vecteur (k:=/ Rsqr (distance I A) * k) (I:=I) (A:=A) (A':=B)) ; auto. assert (I = milieu A C); auto with geo. replace (distance I A) with (distance I C); auto with geo. rewrite (homothetie_vecteur H3). assert (Rsqr (distance I C) <> 0). assert (distance I C <> 0); auto with geo. unfold Rsqr in |- *; auto with real. Ringvec. Qed.