proposition: Lemma Cnorm_INC_lt : forall n m:nat, Cnorm (INC n) < Cnorm (INC m) -> (n < m)%nat.
proof: Proof. induction n; induction m. - simpl. intro Habs. lra. - revert m IHm. intros n1 H1 H2. destruct n1. intuition. constructor. assert (Hind : (0<S n1 -> 1 <= S n1)%nat). intuition. apply Hind. apply H1. rewrite S_INC. generalize (Cre_INC_pos n1). generalize (Cim_INC_0 n1). intros Hu Hs. destruct (INC n1). simpl in *. apply sqrt_lt_1. unfold Cnorm_sqr. simpl. apply Cnorm_sqr_pos. unfold Cnorm_sqr. apply Cnorm_sqr_pos. unfold Cnorm_sqr. simpl. rewrite <- Hu. ring_simplify. apply Rplus_le_lt_0_compat. apply Rplus_le_le_0_compat. replace (r^2)%R with (Rsqr r) by (compute; ring). apply Rle_0_sqr. replace (IZR 0) with (2*0)%R by ring. apply Rmult_le_compat_l. lra. assumption. lra. - revert n IHn. intros n0 H1 H2. rewrite S_INC in H2. generalize (Cre_INC_pos n0). generalize (Cim_INC_0 n0). intros Hu Hs. destruct (INC n0). simpl in *. apply sqrt_lt_0 in H2. unfold Cnorm_sqr in *. simpl in *. rewrite <- Hu in H2. ring_simplify in H2. assert (H : 0<= (Rsqr (r+1))%R). apply Rle_0_sqr. destruct H. compute in H. ring_simplify in H. assert (H0 : (forall x: R, x > 0 -> x < 0 -> False)). intros. lra. assert (Habs : ((0 < r ^ 2 + 2 * r + 1) -> (r ^ 2 + 2 * r + 1 < 0)->False)%R). apply H0. destruct Habs ; assumption. rewrite H in H2. compute in H2. ring_simplify in H2. lra. apply Cnorm_sqr_pos. unfold Cnorm_sqr. simpl. apply Cnorm_sqr_pos. - revert n IHn m IHm. intros n1 H3 n0 H1 H4. assert (H : (n1<n0 -> S n1 < S n0)%nat). intuition (auto with arith). apply H. apply H3. do 2 rewrite S_INC in H4. generalize (Cre_INC_pos n0). generalize (Cim_INC_0 n0). intros Hu Hs. generalize (Cre_INC_pos n1). generalize (Cim_INC_0 n1). intros Hu1 Hs1. destruct (INC n0) ; destruct (INC n1). simpl in *. apply sqrt_lt_1. apply sqrt_lt_0 in H4. apply Cnorm_sqr_pos. apply Cnorm_sqr_pos. apply Cnorm_sqr_pos. apply Cnorm_sqr_pos. rewrite <- Hu in *. rewrite <- Hu1 in *. apply sqrt_lt_0 in H4. ring_simplify in H4. unfold Cnorm_sqr in *. simpl in *. ring_simplify in H4. ring_simplify. generalize H4. replace (r1 ^ 2 + 2 * r1 + 1)%R with (Rsqr (r1 + 1))%R by (compute; ring). replace (r ^ 2 + 2 * r + 1)%R with (Rsqr (r + 1))%R by (compute; ring). replace ( r1 ^ 2)%R with (Rsqr r1) by (compute ; ring). replace ( r ^ 2)%R with (Rsqr r) by (compute ; ring). intro H5. apply Rsqr_incrst_0 in H5. apply Rsqr_incrst_1. lra. exact Hs1. exact Hs. lra. lra. apply Cnorm_sqr_pos. apply Cnorm_sqr_pos. Qed.
imports: Ctacfield Cbase Cpow Lia