proposition: Theorem inversion_pole_origine_complexe : forall (k : R) (z z' : C) (M M' : PO), O <> M :>PO -> k <> 0 -> z = affixe_vec (vec O M) :>C -> z' = affixe_vec (vec O M') :>C -> M' = inversion O k M :>PO -> z' = Cmult (Rinj k) (Cinv (Conj z)).
proof: Proof. intros. elim Rtotal_order with (r1 := k) (r2 := 0); [ intros H4; try clear total_order | intros H4; elim H4; [ intros H5; try clear H4 total_order; try exact H5 | intros H5; try clear H4 total_order ] ]. rewrite (inversion_negatif_complexe (k:=k) (z:=z) (z':=z') (M:=M) (M':=M')); auto. absurd (k = 0); auto. rewrite (inversion_positif_complexe (k:=k) (z:=z) (z':=z') (M:=M) (M':=M')); auto. Qed.