proposition: Lemma Cnorm_le_INC : forall n m:nat, (n <= m)%nat -> Cnorm (INC n) <= Cnorm (INC m).
proof: Proof. intros n m H. induction H. right. reflexivity. apply Rle_trans with (Cnorm (INC m)). exact IHle. left. apply Cnorm_lt_INC. intuition. Qed.
imports: Ctacfield Cbase Cpow Lia