proposition: Lemma Cre_INC_pos : forall n : nat, 0 <= Cre (INC n).
proof: Proof. induction n. intuition (auto with real). rewrite S_INC. destruct (INC n); simpl in *. intuition (auto with real). Qed.
imports: Ctacfield Cbase Cpow Lia