proposition: Lemma Rinj_Cinv : forall k : R, k <> 0 -> Rinj (/ k) = Cinv (Rinj k).
proof: Proof. intros. assert (Rinj k <> zeroC); auto with geo. assert (Cmult (Rinj k) (Rinj (/ k)) = oneC). 2: symmetry in |- *; apply Cinv_def2; auto. unfold Rinj, oneC in |- *. rewrite Cmult_algebrique. replace (0 * / k + k * 0) with 0 by (field;auto). replace (k * / k + - (0 * 0)) with 1 by (field;auto). auto. Qed.