proposition: Lemma not_0_INC : forall n:nat, n <> 0%nat -> INC n <> 0.
proof: Proof. induction n. intuition. intro H. rewrite S_INC. generalize (Cre_INC_pos n). intro H1. destruct (INC n). simpl in *. rewrite <- Ceq. simpl. intuition. lra. Qed.
imports: Ctacfield Cbase Cpow Lia