proposition: Lemma Cnorm_lt_1_INC : forall n:nat, (1 < n)%nat -> 1 < Cnorm (INC n).
proof: Proof. intros n H. induction n. inversion H. rewrite S_INC. destruct n. inversion H. inversion H1. rewrite S_INC in IHn. rewrite S_INC. generalize (Cre_INC_pos n). generalize (Cim_INC_0 n). intros H2 H3. destruct (INC n); simpl in *. rewrite <- sqrt_1. apply sqrt_lt_1. lra. apply Cnorm_sqr_pos. unfold Cnorm_sqr ; simpl. rewrite <- H2. apply Rminus_gt. unfold Cnorm_sqr. ring_simplify. unfold Rminus ; rewrite Rplus_assoc ; apply Rplus_le_lt_0_compat. apply Rmult_le_pos ; [| rewrite Rmult_1_r] ; assumption. replace R0 with (4*0)%R by ring. lra. Qed.
imports: Ctacfield Cbase Cpow Lia