proposition: Theorem ecriture_complexe_inversion : forall (k : R) (j z z' : C) (J M M' : PO), J <> M -> k <> 0 -> z = affixe M -> z' = affixe M' -> j = affixe J -> (M' = inversion J k M <-> Cplus z' (Copp j) = Cmult (Rinj k) (Cinv (Conj (Cplus z (Copp j))))).
proof: Proof. intros; red in |- *; try split; intros. apply (inversion_complexe (k:=k) (j:=j) (z:=z) (z':=z') (J:=J) (M:=M) (M':=M')); auto. apply (complexe_inversion (k:=k) (j:=j) (z:=z) (z':=z') (J:=J) (M:=M) (M':=M')); auto. Qed.