proposition: Lemma INC_inv_Cim_INR : forall n : nat, n <> 0%nat -> Cim (/INC n) = 0%R.
proof: Proof. intros n Hn. unfold Cinv. simpl. repeat rewrite <- Cim_INC_0. repeat rewrite Cre_INC_INR. field. apply not_0_INR. exact Hn. Qed.
imports: Ctacfield Cbase Cpow Lia