proposition: Lemma Cnorm_lt_INC : forall n m:nat, (n < m)%nat -> Cnorm (INC n) < Cnorm (INC m).
proof: Proof. intros n m H. induction H. generalize (Cre_INC_pos n). generalize (Cim_INC_0 n). intros H1 H2. rewrite S_INC. destruct (INC n). simpl in *. apply sqrt_lt_1. apply Cnorm_sqr_pos. apply Cnorm_sqr_pos. unfold Cnorm_sqr. simpl. ring_simplify. do 2 rewrite Rplus_assoc. apply (Rplus_lt_compat_l (r^2)). rewrite <- H1. ring_simplify. apply Rplus_le_lt_0_compat. replace (IZR 0) with (2*0)%R by ring. apply Rmult_le_compat_l. lra. assumption. lra. rewrite S_INC. apply Rlt_trans with (Cnorm (INC m)). exact IHle. generalize (Cre_INC_pos m). generalize (Cim_INC_0 m). intros H1 H2. destruct (INC m). simpl in *. apply sqrt_lt_1. apply Cnorm_sqr_pos. apply Cnorm_sqr_pos. unfold Cnorm_sqr. simpl. ring_simplify. do 2 rewrite Rplus_assoc. apply (Rplus_lt_compat_l (r^2)). rewrite <- H1. ring_simplify. apply Rplus_le_lt_0_compat. replace (IZR 0) with (2*0)%R by ring. apply Rmult_le_compat_l. lra. assumption. lra. Qed.
imports: Ctacfield Cbase Cpow Lia