proposition: Lemma Cim_INC : forall n, Cim (INC n) = 0%R.
proof: Proof. intros n. induction n. intuition. rewrite S_INC. rewrite <- Cim_add_compat. rewrite IHn. simpl. intuition (auto with real). Qed.
imports: Ctacfield Cbase Cpow Lia